Interface:First-order logic with quantifiability

First-order logic with quantifiability

This interface collects important theorems from first-order logic, which builds on propositional logic by adding quantifiers ("for all" and "there exists") and equality. It is meant as a user-friendly reservoir for those interfaces and proof modules which merely use first-order logic, without proving anything new within it. It also includes results which rely on the axiom of quantifiability, such as most of the ones involving substituting a term for a variable. Statements can be added if necessary, but then the exporting modules have to be updated accordingly.

Module usage
Parameters
Interface:Classical propositional calculus
Imported by
Interface:Peano axioms Interface:Tarski's geometry axioms and others
Exported by
First-order logic with quantifiability First-order logic in terms of substitution built on equality

Formulas, objects, and quantification

We build on Interface:Classical propositional calculus:

param (CLASSICAL Interface:Classical_propositional_calculus () ())

By convention we use φ, ψ, χ, and θ to represent formulas:

var (formula φ ψ χ θ φx φs φy antecedent)

We use the term object to refer to something which is subject to quantification or equality. From an axiomatic point of view, what is a valid object is defined implicitly, by axioms such as those of ZFC set theory or Peano arithmetic.

kind (object)
var (object s t u s0 s1 t0 t1)

A variable is something we can quantify over.

kind (variable)
var (variable x y z x0 x1 y0 y1)

A variable can be used where an object is expected, although it needs to be converted via the following explicit conversion. When we are writing informally (rather than in JHilbert proofs themselves), we may omit the conversion (it should be understood whereever we use a variable in a context where an object is expected).

term (object (value variable))

The reverse is not possible. Examples of objects which are not variables might be s + t for Peano arithmetic, or s ∪ t for set theory.

We extend the available formulas with universal quantification and existential quantification:

term (formula (∀ variable formula))
term (formula (∃ variable formula))

Relationship between universal and existential quantification

stmt (NotForAll () () ((¬ (∀ x φ)) ↔ (∃ x (¬ φ))))
stmt (NotThereExists () () ((¬ (∃ x φ)) ↔ (∀ x (¬ φ))))

Builders for quantifiers

As with propositional calculus, we need to build up formulas explicitly, and these rules let us do it. We provide them for both quantifiers, for implication and the biconditional.

stmt (addForAll () ((φ → ψ)) ((∀ x φ) → (∀ x ψ)))
stmt (addThereExists () ((φ → ψ)) ((∃ x φ) → (∃ x ψ)))

stmt (buildForAll () ((φ ↔ ψ)) ((∀ x φ) ↔ (∀ x ψ)))
stmt (buildThereExists () ((φ ↔ ψ)) ((∃ x φ) ↔ (∃ x ψ)))

Additional builders

Some of these builders rely on theorems we haven't presented yet, but they are similar to the simple ones above in terms of general intent.

stmt (buildThereExistsInConsequent ((x φ)) 
  ((φ → (ψ ↔ χ)))
  (φ → ((∃ x ψ) ↔ (∃ x χ))))
stmt (buildForAllInConsequent ((x φ))
  ((φ → (ψ ↔ χ)))
  (φ → ((∀ x ψ) ↔ (∀ x χ))))

Order

The order of adjacent quantifiers of the same type can be exchanged:

stmt (ForAllCommutation () () ((∀ x (∀ y φ)) ↔ (∀ y (∀ x φ))))
stmt (ThereExistsCommutation () () ((∃ x (∃ y φ)) ↔ (∃ y (∃ x φ))))

∃ followed by ∀ can be switched,

stmt (ThereExistsForAllCommutation () () ((∃ x (∀ y φ)) → (∀ y (∃ x φ))))

but the converse does not in general hold.

Combining quantified statements

Quantifiers of the same variable can sometimes be combined or split:

stmt (ForAllConjunction () () ((∀ x (φ ∧ ψ)) ↔ ((∀ x φ) ∧ (∀ x ψ))))
stmt (ThereExistsDisjunction () () ((∃ x (φ ∨ ψ)) ↔ ((∃ x φ) ∨ (∃ x ψ))))
stmt (ThereExistsImplication () () ((∃ x (φ → ψ)) ↔ ((∀ x φ) → (∃ x ψ))))
stmt (ForAllImplication () () ((∀ x (φ → ψ)) → ((∀ x φ) → (∀ x ψ))))
stmt (ThereExistsConjunction () () ((∃ x (φ ∧ ψ)) → ((∃ x φ) ∧ (∃ x ψ))))

Biconditional

stmt (ForAllBiconditional () () ((∀ x (φ ↔ ψ)) → ((∀ x φ) ↔ (∀ x ψ))))

Other kinds of splits and combinations

stmt (ForAllImplicationThereExists () () ((∀ x (φ → ψ)) → ((∃ x φ) → (∃ x ψ))))
stmt (ForAllBiconditionalThereExists () () ((∀ x (φ ↔ ψ)) → ((∃ x φ) ↔ (∃ x ψ))))

stmt (ThereExistsConjunctionCombining () ()
  (((∀ x φ) ∧ (∃ x ψ)) → (∃ x (φ ∧ ψ))))
stmt (ThereExistsConjunctionRightCombining () ()
  (((∃ x φ) ∧ (∀ x ψ)) → (∃ x (φ ∧ ψ))))

stmt (combineThereExistsForAll () ((∃ x φ) (∀ x ψ)) (∃ x (φ ∧ ψ)))

Generalization and specialization

We can remove a universal quantifier:

stmt (Specialization () () ((∀ x φ) → φ))
stmt (specialize () ((∀ x φ)) φ)

The converse is sometimes possible, but only with some restrictions. Either the variable does not occur in the formula, or the formula is unconditionally true:

stmt (Generalization ((x φ)) () (φ → (∀ x φ)))
stmt (generalize () (φ) (∀ x φ))

An existential quantifier can be added unconditionally,

stmt (ThereExistsIntroduction () () (φ → (∃ x φ)))

and can be removed if the variable does not occur in the formula.

stmt (NullThereExists ((x φ)) () ((∃ x φ) ↔ φ))
stmt (removeThereExists ((x φ)) ((∃ x φ)) φ)
stmt (removeThereExistsInConsequent ((x φ)) ((antecedent → (∃ x φ))) (antecedent → φ))

Equality

Equality is reflexive, symmetry, and transitive.

term (formula (= object object))
stmt (EqualityReflexivity () () (s = s))

stmt (EqualitySymmetry () () ((s = t) ↔ (t = s)))
stmt (swapEquality () ((s = t)) (t = s))

stmt (EqualityTransitivity () () (((s = t) ∧ (t = u)) → (s = u)))
stmt (applyEqualityTransitivity () ((s = t) (t = u)) (s = u))

Here are convenience theorems which are closely related to those:

stmt (swapEqualityInConsequent () ((φ → (s = t))) (φ → (t = s)))
stmt (applyEqualityTransitivityInConsequent () ((φ → (s = t)) (φ → (t = u))) (φ → (s = u)))

There is also the principle of "equals can be substituted for equals". In our system, this is done via builders, and here we provide one for equals itself. Theories which build on first-order logic will provide builders for additional expressions such as ∈ (is an element of) for set theory or + (addition) for Peano arithmetic.

stmt (EqualityBuilder () () (((s0 = s1) ∧ (t0 = t1)) → ((s0 = t0) ↔ (s1 = t1))))
stmt (buildEquality () ((s0 = s1) (t0 = t1)) ((s0 = t0) ↔ (s1 = t1)))

We also supply a variety of variant builders, for convenience:

stmt (EqualityBuilderRR () () ((s0 = s1) → ((s0 = t) ↔ (s1 = t))))
stmt (buildEqualityRR () ((s0 = s1)) ((s0 = t) ↔ (s1 = t)))

stmt (EqualityBuilderLL () () ((s0 = s1) → ((t = s0) ↔ (t = s1))))
stmt (buildEqualityLL () ((t0 = t1)) ((s = t0) ↔ (s = t1)))

stmt (buildEqualityInConsequent ()
  ((φ → (s0 = s1))
   (φ → (t0 = t1)))
  (φ → ((s0 = t0) ↔ (s1 = t1))))
stmt (buildEqualityRRInConsequent ()
  ((φ → (s0 = s1)))
  (φ → ((s0 = t) ↔ (s1 = t))))
stmt (buildEqualityLLInConsequent ()
  ((φ → (t0 = t1)))
  (φ → ((s = t0) ↔ (s = t1))))

We also define ≠, which is just an abbreviation for negation and equality.

def ((≠ s t) (¬ (s = t)))

Free variables

We provide a variety of ways to prove that a variable is not free in a formula, and a variety of conclusions that follow from this. These theorems do not depend on the details of how is-not-free-in is defined, and there is no theorem that implies the negation of is-not-free-in for cases not covered here. In other words, is-not-free-in need not correspond exactly to the conventional definition of freeness, as long as it corresponds for the cases we need.

term (formula (is-not-free-in variable formula))

Showing a variable is free

A variable is not free in a formula if it does not occur in the formula:

stmt (DistinctNotFree ((x φ)) () (x is-not-free-in φ))

A variable is not free in a formula if it is bound by a quantifier:

stmt (BoundForAllNotFree () () (x is-not-free-in (∀ x φ)))
stmt (BoundThereExistsNotFree () () (x is-not-free-in (∃ x φ)))

If a variable is not free in a formula it is not free in a formula which adds another quantifier (possibly to a different variable) at the start:

stmt (addForAllNotFree () ((x is-not-free-in φ)) (x is-not-free-in (∀ y φ)))
stmt (addThereExistsNotFree () ((x is-not-free-in φ)) (x is-not-free-in (∃ y φ)))

If a variable is not free in any of the parts of a formula it is not free in the formula which joins them with connectives:

stmt (negateNotFree () ((x is-not-free-in φ)) (x is-not-free-in (¬ φ)))

stmt (implicationNotFree () 
  ((x is-not-free-in φ) (x is-not-free-in ψ))
  (x is-not-free-in (φ → ψ))
)

stmt (disjunctionNotFree () 
  ((x is-not-free-in φ) (x is-not-free-in ψ))
  (x is-not-free-in (φ ∨ ψ)))

stmt (conjunctionNotFree ()
  ((x is-not-free-in φ) (x is-not-free-in ψ))
  (x is-not-free-in (φ ∧ ψ)))

stmt (biconditionalNotFree ()
  ((x is-not-free-in φ) (x is-not-free-in ψ))
  (x is-not-free-in (φ ↔ ψ)))

And we supply a builder for is-not-free-in:

stmt (buildNotFree () ((φ ↔ ψ)) ((x is-not-free-in φ) ↔ (x is-not-free-in ψ)))

Adding or removing quantifiers

If a variable is not free in a formula, it is legitimate to add or remove quantifiers from that formula:

stmt (ForAllAddRemoveNotFree () ((x is-not-free-in φ)) ((∀ x φ) ↔ φ))
stmt (ThereExistsAddRemoveNotFree () ((x is-not-free-in φ)) ((∃ x φ) ↔ φ))

Moving formulas in and out of quantification

The results in this section all have to do with being able to move around formulas relative to quantifiers, given that the quantified variable is not free in the formula being moved.

Implication

stmt (ForAllImplicationAntecedentMovement () ((x is-not-free-in φ)) ((∀ x (φ → ψ)) ↔ (φ → (∀ x ψ))))
stmt (moveAntecedentOutOfForAll () ((∀ x (φ → ψ)) (x is-not-free-in φ)) (φ → (∀ x ψ)))
stmt (moveAntecedentIntoForAll () 
  ((φ → (∀ x ψ)) (x is-not-free-in φ)) 
  (∀ x (φ → ψ)))

stmt (ThereExistsAntecedentMovementNotFree () ((x is-not-free-in φ)) ((∃ x (φ → ψ)) ↔ (φ → (∃ x ψ))))
stmt (ForAllImplicationConsequentMovement () ((x is-not-free-in ψ)) ((∀ x (φ → ψ)) ↔ ((∃ x φ) → ψ)))
stmt (ThereExistsImplicationConsequentMovement () ((x is-not-free-in ψ)) ((∃ x (φ → ψ)) ↔ ((∀ x φ) → ψ)))

stmt (ThereExistsConjunctionMovementNotFree () ((x is-not-free-in φ)) ((∃ x (φ ∧ ψ)) ↔ (φ ∧ (∃ x ψ))))

Versions with distinct variables

stmt (ThereExistsConjunctionMovement ((x φ)) () ((∃ x (φ ∧ ψ)) ↔ (φ ∧ (∃ x ψ))))
stmt (ThereExistsConjunctionRightMovement ((x ψ)) () ((∃ x (φ ∧ ψ)) ↔ ((∃ x φ) ∧ ψ)))

stmt (ThereExistsDisjunctionMovement ((x φ)) () ((∃ x (φ ∨ ψ)) ↔ (φ ∨ (∃ x ψ))))
stmt (ThereExistsDisjunctionRightMovement ((x ψ)) () ((∃ x (φ ∨ ψ)) ↔ ((∃ x φ) ∨ ψ)) )

stmt (ThereExistsAntecedentMovement ((x φ)) () ((∃ x (φ → ψ)) ↔ (φ → (∃ x ψ))))

Here are a few rules based on these:

stmt (moveLeftConjunctIntoThereExistsInConsequent ((x φ))
  ((antecedent → (φ ∧ (∃ x ψ))))
  (antecedent → (∃ x (φ ∧ ψ))))
stmt (moveRightConjunctIntoThereExistsInConsequent ((x ψ))
  ((antecedent → ((∃ x φ) ∧ ψ)))
  (antecedent → (∃ x (φ ∧ ψ))))
stmt (repeatAntecedentThereExists ((x antecedent))
  ((antecedent → (∃ x ψ)))
  (antecedent → (∃ x (antecedent ∧ ψ))))

Scattering and gathering

If we have two formulas joined by a conjunction, one quantified over one variable and the other quantified over another, we can express the quantifiers either at the beginning or with the formulas they apply to. We name the propositions φx and ψy to express the idea that φx will typically contain x and ψy will typically contain y.

var (formula ψy)
stmt (ThereExistsScattering ((φx y) (ψy x)) ()
  ((∃ x (∃ y (φx ∧ ψy))) ↔ ((∃ x φx) ∧ (∃ y ψy))))
stmt (gatherThereExistsInConsequent ((φx y) (ψy x)) ((antecedent → ((∃ x φx) ∧ (∃ y ψy))))
  (antecedent → (∃ x (∃ y (φx ∧ ψy)))))

Adding quantifiers to theorems which are implications

These variants on moving formulas turn out to be used particularly often:

stmt (addThereExistsToAntecedent ((x ψ))
  ((φ → ψ))
  ((∃ x φ) → ψ))
stmt (addForAllToConsequent ((x φ))
  ((φ → ψ))
  (φ → (∀ x ψ)))

stmt (addForAllToConsequentNotFree () ((x is-not-free-in φ) (φ → ψ)) (φ → (∀ x ψ)))

Converting variable to object

We can convert a formula containing a variable x to one containing an object s using the following theorem.

stmt (VariableToObject ((x s) (x φs))
  ((((value x) = s) → (φx ↔ φs))
   φx
  )
  φs)

Substitution

Having a formula which substitutes one variable for another greatly increases the readability of many theorems. For example, a statement of induction will generally apply the same formula with 0, k, k + 1, or n.

This kind of substitution is known as proper substitution as there are some rules about what kinds of substitution are valid. The following theorems enable making proper substitutions.

We first define the subst term:

term (formula (subst object variable formula))

so for example (subst s x φ) can be thought of as a copy of φ in which x is changed to s. In more conventional notation this would be [s / x] φ (or, using a common but potentially ambiguous notation, changing φ(x) to φ(s)).

Building up expressions involving subst

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

stmt (introduceSubst () (φ) (subst s x φ))

From an equality, we can build an equivalence of substitutions:

stmt (SubstBuilderReplacement () ()
  ((s = t) → ((subst s x φ) ↔ (subst t x φ))))
stmt (buildSubstReplacement () ((s = t))
  ((subst s x φ) ↔ (subst t x φ)))

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. The distinct variable constraint between x and s might be one we can eliminate, but in practice it isn't too difficult to deal with.

stmt (makeSubstExplicit ((x s) (x ψ))
  ((((value x) = s) → (φ ↔ ψ)))
  ((subst s x φ) ↔ ψ))

We can add subst to both sides of an implication or a biconditional.

stmt (SubstAddition () () ((∀ x (φ → ψ)) → ((subst s x φ) → (subst s x ψ))))
stmt (SubstBuilder () () ((∀ x (φ ↔ ψ)) → ((subst s x φ) ↔ (subst s x ψ))))

stmt (addSubst () ((φ → ψ)) ((subst s x φ) → (subst s x ψ)))
stmt (buildSubst () ((φ ↔ ψ)) ((subst s x φ) ↔ (subst s x ψ)))

We can move subst across logical connectives,

stmt (SubstNegation () () ((subst s x (¬ φ)) ↔ (¬ (subst s x φ))))
stmt (SubstDisjunction () () ((subst s x (φ ∨ ψ)) ↔ ((subst s x φ) ∨ (subst s x ψ))))
stmt (SubstConjunction () () ((subst s x (φ ∧ ψ)) ↔ ((subst s x φ) ∧ (subst s x ψ))))
stmt (SubstImplication () () ((subst s x (φ → ψ)) ↔ ((subst s x φ) → (subst s x ψ))))
stmt (SubstBiconditional () () ((subst s x (φ ↔ ψ)) ↔ ((subst s x φ) ↔ (subst s x ψ))) )

and quantifiers (to distinct variables).

stmt (SubstThereExists ((x y s)) () ((subst s x (∃ y φ)) ↔ (∃ y (subst s x φ))))

Substitution of a variable which does not appear

stmt (NullSubstitution ((x φ)) () ((subst s x φ) ↔ φ))

Turning substitution into there-exists

One way to prove a formula of the form ∃ x φ is to demonstrate a particular x for which φ holds.

stmt (ThereExistsIntroductionFromObject () () ((subst s x φ) → (∃ x φ)))
stmt (introduceThereExistsFromObject () ((subst s x φ)) (∃ x φ))

Specialization

Specialization as conventionally cited 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 ] φ.

stmt (SpecializationToObject () () ((∀ x φ) → (subst s x φ)))
stmt (specializeToObjectInConsequent () ((antecedent → (∀ x φ))) (antecedent → (subst s x φ)))

Changing the quantified variable

We can transform a quantified formula by substituting each of the occurences of the variable we are quantifying over to another variable, and changing the variable in the quantifier accordingly. Here is a version with implicit substitution,

stmt (ChangeVariableThereExists
  ((y φx) (x φy) (x y))
  ((((value x) = (value y)) → (φx ↔ φy)))
  ((∃ x φx) ↔ (∃ y φy)))
stmt (ChangeVariableForAll ((y φx) (x φy) (x y))
  ((((value x) = (value y)) → (φx ↔ φy)))
  ((∀ x φx) ↔ (∀ y φy)))

and one with explicit substitution.

stmt (ChangeVariableExplicitThereExists ((y φ) (x y)) ()
  ((∃ x φ) ↔ (∃ y (subst (value y) x φ))))
stmt (ChangeVariableExplicitForAll ((y φ) (x y)) ()
  ((∀ x φ) ↔ (∀ y (subst (value y) x φ))))

Here are versions of the implicit ones with explicit freeness hypotheses rather than distinct variable constraints.

stmt (ChangeVariableThereExistsNotFree
  ((x y))
  ((x is-not-free-in φy)
   (y is-not-free-in φx)
   (((value x) = (value y)) → (φx ↔ φy)))
  ((∃ x φx) ↔ (∃ y φy)))
stmt (ChangeVariableForAllNotFree ((x y))
  ((x is-not-free-in φy)
   (y is-not-free-in φx)
   (((value x) = (value y)) → (φx ↔ φy)))
  ((∀ x φx) ↔ (∀ y φy)))

A similar transformation is possible for substitution.

stmt (ChangeVariableSubstitution
  ((y φx) (x φy) (x y) (s x) (s y))
  ((((value x) = (value y)) → (φx ↔ φy)))
  ((subst s x φx) ↔ (subst s y φy)))

More theorems involving subst

stmt (EqualitySubst () () (((value x) = s) → (φ ↔ (subst s x φ))))
stmt (SubstItself () () ((subst (value x) x φ) ↔ φ))

Some theorems related to substitution

Although the following theorems do not refer to substitution with subst, they do express similar ideas.

stmt (ImplicitForAll ((x s) (x ψ)) ((((value x) = s) → (φ ↔ ψ)))
  ((∀ x (((value x) = s) → φ)) ↔ ψ))
stmt (ImplicitThereExists ((x s) (x ψ)) ((((value x) = s) → (φ ↔ ψ)))
  ((∃ x (((value x) = s) ∧ φ)) ↔ ψ))

Quantifiability

Although the above results do imply the axiom of quantifiability, at least on occasion it is useful directly.

stmt (Quantifiability ((x s)) () (∃ x ((value x) = s)) )

References

Interface module parsed successfully