First-order logic with quantifiability

From Wikiproofs

Used interfaces
Imports
Interface:First-order logic Interface:Axiom of quantifiability
Exports
Interface:First-order logic with quantifiability

We start with Interface:Classical propositional calculus and Interface:First-order logic. We don't import the Interface:Axiom of quantifiability yet.

As usual, φ, ψ, χ, and θ are formulas, x, y, and z are variables, and s, t, and u are objects:

Contents 1 Substitution of objects 1.1 Builders 1.1.1 Based on replacement 1.1.2 Implication builder 1.1.3 Biconditional builder 1.2 Proving there-exists 2 Free variables and substitution 3 Axiom of quantifiability 4 Specialization with substitution 5 Quantifiers and equality 5.1 ax9oc 5.2 Implicit substitution and ∀ 5.3 Implicit substitution and ∃ 5.4 Implicit substitution of an object for a variable 5.5 Object version of VariableSubstitution axiom 5.6 Two ways to express substitution when variables are distinct 6 Substitution and ∃ 7 Substitution of a variable which is not free 8 Substitution can be moved across connectives 8.1 Negation 9 Composition 10 equs4c 11 Substitution of objects, with axiom of quantifiability 11.1 Substitution of a theorem remains a theorem 11.2 Convert from implicit substitution 12 Substituting one quantified variable for another 13 Export 14 Footnotes 15 Cited works

[edit] Substitution of objects

We now turn to substitution of an object for a variable.

In some formulations of predicate logic, this kind of substitution (known as proper substitution as there are some rules about what kinds of substitution are valid) is performed syntactically and the rules governing it are expressed in English or a meta-theory. JHilbert does not have a feature to do syntactic proper substitution, but we are able to build up equivalent mechanisms from equality. The theorems in Interface:First-order logic with quantifiability could be proven from either the syntactic definition or ours.

We define a formula (subst s x φ) which means, roughly, that φ is true if ocurrences of x are replaced by s ("roughly" because we have not tried to define proper substitution precisely). In dicussion, we also use the notation [ s / x ] φ (which is not legal JHilbert syntax) for the same thing. The definition is [ s / x ] φ ≝ ∃ y (y = s ∧ ∃ x (x = y ∧ φ)). The definition contains a dummy variable y to give the expected results if x and s are not distinct.^[1]

Currently, the definition of subst is an axiom in Interface:Axiom of quantifiability. Therefore, we import that interface now, even though we aren't going to use the axiom of quantifiability itself for a little while.

This section contains a few of the preliminary results, which we can prove without the axiom of quantifiability.

[edit] Builders

We can build up formulas based on equivalences or equalities of the the substituted proposition or the replacement (that is, φ or s in (subst s x φ), respectively).

[edit] Based on replacement

In this section we will prove s = t → ((subst s x φ) ↔ (subst t x φ)). This is like dfsbcq in set.mm.^[2] The set.mm analogue for substituting a variable (rather than an object) is sbequ.^[3]

Now we just need to apply the definition of subst and we are done:

[edit] Implication builder

Analogous to our other implication builders, this theorem takes an implication and lets us add subst to both sides. The proof is just a straightforward application of the existing builders for conjunction and ∃.

Now we just need to apply the definition of subst and we are done:

[edit] Biconditional builder

The builder for the biconditional is very similar to the implication builder. It could be proved much the way we proved the implication builder, but we derive it from the implication builder.^[4]

[edit] Proving there-exists

One way to prove a formula of the form ∃xφ is to demonstrate a particular x for which φ holds. In constructive logic any theorem ∃xφ can be proved this way (because of the existence property), but even in classical (non-constructive) logic this is one of the most common ways of proving ∃xφ.

In our notation, this idea is expressed via subst:

The proof takes the definition of subst, (∃ y (y = s ∧ (∃ x (x = y ∧ φ)))) and pares it down by eliminating the parts we don't need.

We start with (y = s ∧ ∃ x (x = y ∧ φ)) → ∃ x (x = y ∧ φ)

and ∃ x (x = y ∧ φ) → ∃ x φ:

which by syllogism gives us (y = s ∧ ∃ x (x = y ∧ φ)) → ∃ x φ

We add ∃ y to both sides and simplify ∃ y ∃ x φ to ∃ x φ:

Now we just need to apply the definition of subst and we are done:

[edit] Free variables and substitution

A substitution acts like a quantifier in the sense that it binds the variable being substituted. So this variable is not free in the substituted formula (provided it is not free in the object being substituted for the variable).

The proof consists of just applying our not-free theorems to each piece of the definition of subst

[edit] Axiom of quantifiability

Having gotten about as far as we're going to get without the Interface:Axiom of quantifiability, we now start proving some consequences of it (because that file also contains the definition of subst, we have already imported it).

[edit] Specialization with substitution

The version of Specialization from Interface:First-order logic is not the one most often presented as a theorem (or axiom) of predicate logic. The standard version also contains a substitution, and is often worded something like "if a formula holds for all values of a variable, it also holds when a particular term is properly substituted for that variable" or in symbols ∀ x φ → [ s / x ] φ).^[5][6][7]

We start with ∀ x φ ∧ ∃ x x = y → ∃ x (φ ∧ x = y) and eliminate the second antecedent (because it is an instance of Quantifiability).

Commuting the conjunction in the consequent gives ∀ x φ → ∃ x (x = y ∧ φ)

We are heading towards the definition of [ s / x ] φ, which has two quantifiers: an outer one on y and an inner one on x. So far we have the quantifier for x and a similar set of steps to the ones we just took will give us a similar expression with a quantifier for y.

We add ∃ y y = s (a theorem) to the consequent:

The consequent is ∀ y ∃ x (x = y ∧ φ) ∧ ∃ y y = s), which we first turn into ∃ y (∃ x (x = y ∧ φ) ∧ y = s),

And then into ∃ y (y = s ∧ ∃ x (x = y ∧ φ)).

Now we just need to apply the definition of subst and we are done:

[edit] Quantifiers and equality

Here we prove a number of results involving equality and quantifiers. Many of them will pave the way for results involving explicit (subst) substitution.

[edit] ax9oc

First is a consequence of the Quantifiability axiom:^[8]

This gives us ∀x(x = s → ∀xφ) → (∃x x = s → ∃x∀xφ), which can be simplified to our desired result. The first step is to note that ∃x x = s is just the Quantifiability axiom, and can therefore be removed:

Now we need to reduce ∃x∀xφ to φ:

[edit] Implicit substitution and ∀

A statement of the form x = s → (φ ↔ ψ), where x is not free in ψ, can be thought of as an implicit substitution, as it can be used to relate a formula about x to a formula about s. Here we relate such a statement to ∀x(x = s → φ) (which is one of the formulas we'll be using in manipulating substitutions).^[9]

Starting with x = s → (φ ↔ ψ), we first add ∀x in front of the ψ:

We now distribute the implication over the biconditional to get (x = s → φ) ↔ (x = s → ∀xψ).

The entire formula we have at this point is (x = s → (φ ↔ ψ)) → ((x = s → φ) ↔ (x = s → ∀xψ)). We will add ∀x to the start of each of the three parts.

The left side of that consequent, ∀x(x = s → φ), is the left side of our desired consequent.

We will show that the right side, ∀x(x = s → ∀xψ), is equivalent to ψ. The forward direction is just ax9oc:

The reverse direction is introducing an antecedent and messing around with quantifiers:

Now we just need to combine the forward and reverse directions,

and reassemble our result.

Here's a rule form of basically the same theorem:

[edit] Implicit substitution and ∃

There is a similar result with ∃.^[10]

Our implicit substitution theorem is:

The proof basically consists of massaging negations to derive this result from the corresponding one for ∀. We start by showing that ∀x (x = s → (φ ↔ ψ)) implies that ∀x(x = s → ¬ φ) is equivalent to ¬ ψ.

Now we need to show that ∀x(x = s → ¬ φ) ↔ (¬ ψ) implies ∃x(x = s ∧ φ) ↔ ψ. We first turn the former into ψ ↔ (¬ ∀x(x = s → ¬ φ)):

We stick ψ ↔ ψ on the proof stack for later use,

and work just with ¬ ∀x(x = s → ¬ φ) for now. We move the negation past the quantifier to get ∃x ¬ (x = s → ¬ φ):

Now we turn the negations and implication into a conjunction:

Bringing back two statements we left on the proof stack, we assemble the formula that ∀x(x = s → ¬ φ) ↔ (¬ ψ) is equivalent to ψ ↔ ∃x(x = s ∧ φ),

flip the order to get ∃x(x = s ∧ φ) ↔ ψ,

and combine this with the first part of the proof.

The rule form is:

and a version with distinct variable constraint instead of a freeness hypothesis is:

[edit] Implicit substitution of an object for a variable

Suppose that we have a formula φx and a formula φs which is much the same, but with s in place of x. Then if φx is a theorem, we can conclude φs.

Before we state this more formally, we prove a lemma.

Our main result can be restated as that φx and x = s → (φx ↔ φs) enable us to conclude φs.

[edit] Object version of VariableSubstitution axiom

The VariableSubstitution axiom is stated in terms of substitution of one variable for another. The analogue in which an object is substituted for a variable also holds.

The general idea of the proof is to "substitute" s for y using a formula of the form y = s → (a formula with y in it ↔ much the same formula, but with s).

We start with our substitution, y = s → ((x = y → (φ → ∀ x (x = y → φ))) ↔ (x = s → (φ → ∀ x (x = s → φ))))

Now we apply VariableToObject to convert the axiom to our desired result.

[edit] Two ways to express substitution when variables are distinct

In previous sections, we have seen that ∃ x (x = s ∧ φ) and ∀ x (x = s → φ) behave similarly. In fact, as long as x and s are distinct, they are completely equivalent.^[11]

First we stick something on the proof stack for later use:

The proof consists of first proving x = s → (φ ↔ ∀ x (x = s → φ)),

and then turning this implicit substitution into its ∃ form.

[edit] Substitution and ∃

We've already seen that ∃ x (x = s ∧ φ) is closely related to substitution. Here we show that it is equivalent to [ s / x ] φ, as long as x does not appear in s.

We start with applying some builders to get y = s → (∃ x (x = y ∧ φ) ↔ ∃ x (x = s ∧ φ)).

ImplicitThereExists then gives us ∃ y (y = s ∧ ∃ x (x = y ∧ φ)) ↔ ∃ x (x = s ∧ φ), which is our desired result by the definition of subst.

Now we just need to apply the definition of subst and we are done:

[edit] Substitution of a variable which is not free

Substituting a formula with a variable which is not free in that formula has no effect.^[12]

We begin with [s / x] φ → ∃ x (x = s ∧ φ). The distinct variable constraint between x and s might not be needed.

Since x is not free in φ, ∃ x (x = s ∧ φ) in turn implies ∃ x x = s ∧ φ

We can eliminate the left hand side of the consequent to get [s / x] φ → φ, which is the forward half of our desired result.

The reverse direction is easier. Generalization gets us φ → ∀ x φ, and SpecializationToObject turns that into [s / x] φ

Combining the forward and reverse directions finishes the proof.

[edit] Substitution can be moved across connectives

Substituting a formula consisting of a logical connective is equivalent to substituting each of the operands of that connective.

[edit] Negation

For negation, this is [ s / x ] ¬ φ ↔ ¬ [ s / x ] φ.^[13]

The proof consists of just moving negation around (via the following lemma) and applying ThereExistsForAll.

[edit] Composition

If we first substitute y for x, and then substitute s for y, the whole process is equivalent to substituting s for x (subject to some distinct variable constraints).^[14]

The proof consists of rewriting both of the substitutions on the left hand side via SubstitutionThereExists. First we show [ s / y ] [ y / x ] φ ↔ ∃ y (y = s ∧ [ y / x ] φ).

The second invocation of SubstitutionThereExists shows that the right hand side of that expression is equivalent to ∃ y (y = s ∧ ∃ x (x = y ∧ φ))

But ∃ y (y = s ∧ ∃ x (x = y ∧ φ)) is [ s / x ] φ, by definition.

[edit] equs4c

This is an analogue to equs4 from First-order logic but for objects not variables:

That gives us ((∀ x ((x = y) → φ)) ∧ x = y) → (¬ ((x = y) → (¬ φ))). We transform the consequent to (¬ (∀ x ((x = y) → (¬ φ)))):

And then we add ∀x to the front of that consequent:

We export and add one more ∀x:

which gives us (∀x(x = s → φ) → ∀x(x = s → ∀x ¬ ∀x(x = s → ¬ φ))). The consequent of that is just what we need to apply ax9oc:

so we have simplified the consequent to ¬ ∀x(x = y → ¬ φ)). We merely apply equs3 to that and we're done.

[edit] Substitution of objects, with axiom of quantifiability

The axiom of quantifiability allows us to prove more substitution results because we can assume that a variable can take on a value corresponding to any object.

[edit] Substitution of a theorem remains a theorem

If we have a theorem, we can add a variable substitution onto it.

[edit] Convert from implicit substitution

A statement of the form x = s → (φ ↔ ψ), where x is not free in ψ, can be thought of as an implicit substitution, as it can be used to relate a formula about x to a formula about s.

Although the distinct variable constraint between x and s should not be necessary (if we wanted to require that x and s are distinct we could have a simpler definition of subst), even the version with the constraint can be useful.

The proof will basically consist of two applications of ImplicitSubstitutionThereExists.

First we rewrite x = s → (φ ↔ ψ) as y = s → (x = y → (φ ↔ ψ))

Now we add ∀x to the consequent:

The first application of ImplicitSubstitutionThereExists turns ∀x(x = y → (φ ↔ ψ)) into (∃x x = y ∧ φ) ↔ ψ:

Combining these results gets y = s → ((∃x x = y ∧ φ) ↔ ψ):

We then apply ImplicitSubstitutionThereExists again to get ∃ y (y = s ∧ (∃x x = y ∧ φ)) ↔ ψ), which is our desired result.

Now we just need to apply the definition of subst and we are done:

[edit] Substituting one quantified variable for another

If we have a quantified formula, and we substitute the quantified variable for another (using subst), the formula holds with the substituted variable in the quantifier. In symbols, this is ∀ x φ ↔ ∀ y [ y / x ] φ and ∃ x φ ↔ ∃ y [ y / x ] φ, where y is not free in φ.^[15]

For now, we just prove one direction of these.

An application of SpecializationToObject gives us ∀ x φ → [ y / x ] φ; we just need to observe that y is not free in ∀ x φ, which enables us to add the missing ∀ y.

That gives us ¬ ∀ y [ y / x ] ¬ φ → ¬ ∀ x ¬ φ, and we just need to move around the negations to get our desired result. We start with the consequent.

The antecedent is similar but has one more step because of the substitution.

Here is a version with implicit substitution. Think of φx and φy as two versions of the same formula, but where x has been changed to y. More formally, y does not appear in φx, x does not appear in φy, and x = y → (φx ↔ φy). This lets us conclude ∃ y φy ↔ ∃ x φx.

The (x y) distinct variable constraint is subject to the same commentary as (x s) in makeSubstExplicit (that is, that it might not be necessary).

We first prove the reverse implication.

First we show ∃ y φy → ∃ y [ y / x ] φx.

We then transform the right hand side to ∃ x φx, and we are done.

The reverse direction is an easy consequence, but to prove it we do need to commute the equality and the biconditional.

[edit] Export

That gives us Interface:First-order logic with quantifiability, which we now export.

[edit] Footnotes

1. ↑ It resembles dfsb7 in metamath's set.mm, accessed March 8, 2010, except that s (the replacement) is an object rather than a variable.
2. ↑ dfsbcq in metamath's set.mm, accessed March 7, 2010
3. ↑ sbequ in metamath's set.mm, accessed June 20, 2010
4. ↑ Similar to sbbii in metamath's set.mm, accessed February 24, 2010, except that s is an object not a variable
5. ↑ stdpc4 in metamath's set.mm, accessed June 9, 2010
6. ↑ a5sbc in Raph Levien's Peano, accessed June 9, 2010
7. ↑ Hirst and Hirst, axiom 4 on page 51
8. ↑ like ax9o in metamath's set.mm, accessed February 22, 2010, but for an object not a variable
9. ↑ equsal in metamath's set.mm, accessed May 11, 2010, but for an object not a variable
10. ↑ equsex in metamath's set.mm, accessed March 9, 2010, with s (the replacement) changed from a variable to an object
11. ↑ sb56 in metamath's set.mm, accessed June 17, 2010, except that s is an object rather than a variable
12. ↑ sbf, metamath's set.mm, accessed July 20, 2010, except that the replacement is an object not a variable
13. ↑ sbn in metamath's set.mm, accessed 2010, except that s is an object rather than a variable
14. ↑ sbcco in Raph Levien's Peano, accessed 12 Jun 2010. I don't know why the (x y) distinct variable constraint is missing from that version; the second invocation of sbc5 would seem to require it.
15. ↑ sb8 and sb8e in metamath's set.mm, accessed June 24, 2010

[edit] Cited works

Hirst, Holly P. and Hirst, Jeffry L. (2008-2009 Edition), A Primer for Logic and Proof, self-published on the web by Jeff Hirst

Proof module parsed successfully