Predicate Calculus

Here we describe an example (C6.1) of a Proof Calculus (תחשיב הוכחה), which is complete. This is kind of expansion of the proof calculus described in Propositional Calculus

Characterization

Language

• Connectives $\neg ,\to$
• Quantifier $\forall$

Logical Axioms

Note: The logical axioms (as opposed to the axioms of a concrete theory $K$) can be formulas that are not sentences, and therefore, in proof sequences, there may also be formulas with free variables.

The set $\Lambda$ of logical axioms consists of

Taulogical Axioms

These axioms are from Propositional Calculus, but here $\phi ,\psi ,\theta$ can be formulas of predicate of logic

		Taulogical Axioms
Ax1		$[\phi \to (\psi \to \phi )]$
Ax2		$[\phi \to (\psi \to \theta )]\to [(\phi \to \psi )\to (\phi \to \theta )]$
Ax3	Contrapositive	$[(\neg \phi \to \neg \psi )\to (\psi \to \phi )]$

Axioms of ∀

		Axioms of $\forall$
Ax.4	אקסיומת ההצבה	$\forall x\phi \to \phi [t/x]$	if no variable occur in $t$ become bonud
Ax.5	הזזת הכמת	$\forall x(\phi \to \psi )\to (\phi \to \forall x\psi )$	if $x$ is not occur freely in $\phi$

Axioms of Equality

If it is first-order logic with equality, then we have also

		Equivalence Axioms
Ax.6a	Reflexivity	$\forall x(x=x)$
Ax.6b	Symmetry	$\forall x\forall y(x=y\to y=x)$
Ax.6c	Transitivity	$\forall x\forall y\forall z(x=y\wedge y=z\to x=z)$
		אקסיומות ההחלפה
		(For each n-place function / prediacte symbol)
Ax.7a		\begin{align}\forall v_{0}\forall v_{1}\dots \forall_{2n-2}\forall_{2n-1}(((v_{0}=v_{n})\land\dots \land(v_{n-1}=v_{2n-1}))\to\\(F(v_{0},\dots,v_{n-1})=F(v_{n},\dots,v_{2n-1})))\end{align}
Ax.7b		\begin{align}\forall v_{0}\forall v_{1}\dots \forall_{2n-2}\forall_{2n-1}(((v_{0}=v_{n})\land\dots \land(v_{n-1}=v_{2n-1}))\to\\(P(v_{0},\dots,v_{n-1})\leftrightarrow P(v_{n},\dots,v_{2n-1})))\end{align}

Rules of inference

• Universal Generalization $\frac{\phi }{\forall x\phi }$
• Modus Ponens $\frac{\phi ,(\phi \to \psi )}{\psi }$

Definitions

Here are some definitions related to this proof calculus:

Proof Sequence

• (c6.1) A proof sequence (סדרת הוכחה) from a theory $K$ (in this proof calculus) is a sequence of formulas such that each formula in the sequence is either:
  • A logical axiom (in this proof calculus)
  • A sentence in the set $K$
  • Derived from two previous formulas in the sequence using one of the rules of inference

See also more general defitnion of proof sequence (in some proof claculus)

Note: Here we restrict a theory to be set of sentences. but there are definitions without this restriction. Also, in a proof sequence (unlike to a theory), may be formulas that are not sentences.

Provable Formula

• (syntactic consequence) A formula $\phi$ is theorem (משפט) of $K$ (or is provable (יכיח) from $K$) and denoted by $K⊢\phi$, if and only if, there exists a proof sequence from $K$ such that $\phi$ is the last formula

Theory

• Given a set of sentences $K$
  • $K$ is inconsistent if there exists a sentence $\phi$ s.t. $K⊢\phi$ and $K⊢\neg \phi$
  • $K$ is consistent if it is not inconsistent
  • $K$ is maximally consistent if every superset of $K$ is inconsistent
• A consistent set of sentences is called a theory (תורה)
• (syntactical completeness) A theory $K$ is complete (שלמה) if for every sentence $\phi$, either $K⊢\phi$ or $K⊢\neg \phi$

Usually a theory is understood to be closed under the relation of logical implication. Some accounts define a theory to be closed under the semantic consequence relation, (i.e. if $K\models \phi$, then $\phi \in K$), while others define it to be closed under the syntactic consequence, (i.e. if $K⊢\phi$, then $\phi \in K$). wikipedia

Henkin Theory

• A complete theory $K$ is said to be a Henkin theory if the following condition holds: “If $K$ contains the sentence $\neg \forall x\phi$ then there is a constant $c\in L$ for which $K$ contains $\neg \phi [c/x]$“. (The constant $c$ is called a Henkin witness for $\neg \forall x\phi$)

Properties

Properties of and theorems about this proof calculus:

• (6.1) Every first-order tautology is provable
• (6.2) Soundness Theorem - This proof calculus is sound, i.e.
  • for every set of formulas $K$, and a formula $\phi$, If $K⊢\phi$ (provable), then $K\models \phi$ (logically implied)
• Given $K$ is a theory, $\psi$ is a sentence and $\phi$ is a formula.
  • (6.3) Deduction theorem - If $K\cup \{\psi \}⊢\phi$ then $K⊢(\psi \to \phi )$
  • (6.4a) Principle of explosion - $\{\psi ,\neg \psi \}⊢\phi$ (thus, every inconsistent set of sentences prove every formula)
  • (6.4b) if $K\cup \{\neg \phi \}$ is inconsistent then $K⊢\phi$ (is it iff?todo )
  • (6.5a) if $K⊢\forall x\phi$ and the variable $v$ does not appear in $\phi$ then $K⊢\forall y\phi [y/x]$
  • (6.5b) Given the constant $c$ that does not appear neither in the sentences of $K$ nor in $\phi$. If $K⊢\phi [c/x]$ then $K⊢\forall x\phi$
• Given $L^{\prime }$ a language that adds constants to a language $L$, and $K$ a set of sentences in $L$
  • (6.5c) for every sentence $\phi$ in $L$, if $K⊢\phi$ in $L^{\prime }$ then $K⊢\phi$ in $L$
  • (6.5d) if $K$ is consistent in $L$, then it is consistent in $L^{\prime }$
• Completeness Theorem
  • (6.6) (without equality)
    • (A.) Every theory $K$ in a language $L$ can be extended to a Henkin theory in a language $L^{\prime }$ such that $L^{\prime }$ adds only constants to $L$.
    • (B.) For every Henkin theory in a language $L^{\prime }$, there exists a model in $L^{\prime }$. Reducing the model to the language $L$ gives a model of the theory $K$ in the language $L$.
  • (6.8) (with equality)
    • For every consistent set of sentences has a model in which the relation "$=$" is interpreted as the identity relation