FOL

• GETFOL is an interactive reasoning system. It can be used in many ways, for instance as a programming language for building intelligent systems, as an interactive theorem prover for first order logic or as an environment for the study of mathematical theory of computation.
• GETFOL by Fausto Giunchiglia is built on top of a complete re-implementation of the FOL system by Richard Weyhrauch.
• GETFOL is maintained as a service to researchers interested in logic based representation theory.

What's here:

• Prolegomena
• Diagonalisation Lemma
• Playground

Prolegomena

What's here:

• Section 2: Syllogism
• Section 6: Rewrites
• Section 9: Reflection Principle
• Appendix A: Axiomatization of Natural Numbers
• Appendix B: Axiomatization of S-Expressions
• Appendix D: Semantic Evaluation
• Appendix E: Syntactic Simplification

These examples are inspired from Weyhrauch's Prolegomena to a Theory of Formal Reasoning (PDF).

Section 2: Syllogism

Section 6: Rewrites

• We compute factorial with rewrites.
• We define factorial axiomatically.
• We also define predecessor on successor (the only case needed by factorial) axiomatically.
• We use two helper facts that help rewrite the factorial conditional to take one of the zero or non-zero branches.
• We can now rewrite any factorial call into a peano number.

Section 9: Reflection Principle

“Change theorem proving in the theory into evaluation in the metatheory.”

We can create object theorems at the meta level. We are free, though not encouraged, to create erroneous ones! Here, we have sound and unsound versions of a reflective procedure that asserts the conjunction of two arguments. In the sound version, these arguments must be given as facts, which are guaranteed to be true, while in the unsound version, these arguments are given as well-formed formulas, which can be either true or false.

Section 9.1: Linear Equations

We add a theory of minus \(-\).

We have some linear equations.

Assuming the following theorems, we can solve by hand.

Let us switch to the meta level, and do some algebra.

• We will say (not prove) that:
  • \(x + n = m\) is \(x=m-n\) (if still non-negative)
  • and \(x - n = m\) is \(x=m+n\) (always valid).
• We will require that:
  1. the equation has one of the shapes above,
  2. including \(n\) and \(m\) are literal numbers
  3. for \(x=m-n\) we ensure that \(n<=m\).
• We will give a solved answer of the form \(x=n\). That is, we do all the checking and computation at the meta level.

The 3 next axioms are close to the formulation in the paper.

Back at the object level, we can solve the linear equations with a single reflective call.

Appendix A: An Axiomatization of Natural Numbers

Appendix B: An Axiomatization of S-Expressions

Appendix D: Semantic Evaluations

Appendix E: Syntactic Simplification

(top, beg)

Diagonalisation Lemma

By Alex Simpson, October 1989. Based on the original version by Fausto Giunchiglia.

Would be nicer with reflection up and a mechanism for definitions.

What's here:

• Unformalised Theorem
  • Proof
• Unformalised Theorem
  • Basic Object Theory
  • Basic Meta Theory
  • Encoding
  • Substitution Function
  • Proof

Unformalised Theorem

The diagonalisation lemma is a major step in the proof of many important metamathematical results such as Godel's two theorems. Although not explicitly formulated by Godel the result is just an application of the methods which he developed in his proof.

In its usual form the lemma applies to any first order theory with enough expressive power to represent all primitive recursive functions. The proper proof of the lemma requires a laborious encoding of the expressions of the language as objects of the theory (Godel numbering). Due to the expressive power of the theory meta-theoretical operations on expressions of the language (in particular substitution) are representable in the theory as functions operating on the codes of those expressions. Once the relevant substitution function is established the interesting part of the proof, the diagonal construction, is possible.

The theorem states that for any wff \(\Psi\) with one free variable there is a sentence \(\Phi\) such that:

Here \(\sim.\sim\) represents the code of its argument, \(\Psi[t]\) represents the wff \(\Phi\) with each occurence of its free variable replaced by the term t, and \(\vdash\) is the provability turnstile.

The GETFOL proof will start with the assumption that the relevant substitution function exists. An encoding of the language into the theory is thus assumed (it is necessary for a substitution function to be possible) but the details of the encoding need not be made explicit. The only requirement is that the following holds for each wff \(W\), variable \(v\) and code \(n\):

Here \(W[n/v]\) represents the wff \(W\) with all free occurrences of \(v\) replaced by \(n\).

The stipulation that \(n\) be a code in (*) is crucial. The basic substitution function, subst', satisfies:

where \(t\) is an arbitrary term. However this substitution is not sufficient for diagonalisation because the proof requires the third argument itself to be substituted, rather than what it encodes.

It is obviously impossible to have a function subst'' satisfying:

because different terms representing the same object evaluate equally on the left and differently on the right. The problem is solved in Peano Arithmetic, for example, because only natural numbers are dealt with. Each natural number is canonically represented by its numeral and so the existence of subst satisfying (*) (where \(n\) represents a numeral) follows from subst' satisfying (**) because the encoding of the numerals is primitive recursive and thus representable in the theory.

To make the setting of the diagonalisation lemma as general as possible only the existence of a coding and substitution function satisfying (*) are assumed. Perhaps a more elegant way would be to have a substitution satisfying (**) and a function which encodes a code and then to define:

Proof

Given an arbitrary wff \(\Psi\) with one free variable the construction of a sentence \(\Phi\) which satisfies (DIAG) proceeds in the folowing way:

First an arbitrary variable, say \(v_0\), is selected. It must have a code \(\sim v_0\sim\) so it is possible to construct the wff:

Here the \(\iff\) means that \(\Theta\) is defined to be this wff. \(\Theta\) is not part of the language, it is meta-level abbreviation for the wff it represents.

Putting \(W = \Theta, v = v_0, n = \sim\Theta\sim\) in (*) gives:

Using the definition of \(\Theta\) the following holds:

Here the \(==\) means that the two sides are identical wffs, and the equivalence is derived by performing the substitution on the left hand side.

Because the two sides of (B) are identical wffs their codes are identical, therefore substituting in (A) gives:

Defining \(\Phi\) by

gives:

which is just (C) rewriten using the definition.

But trivially:

because the left hand side is just an abbreviation for the right.

Now substituting via (D) in (E) shows that \(\Phi\) is indeed the required wff.

GETFOL Formalisation

Basic Object Theory

The object theory is a standard unsorted (ie. one sort only) first order theory. For now no assumptions are being made about the language.

Basic Meta Theory

The objects of the meta theory are the names of the object theory expressions - ie. a representation of the lexical forms of the expressions.

Syntax

Semantics

Basic Axiom

If there was reflection up this axiom would not be necessary.

Encoding

The encoding is a mapping from the names of expressions onto the names of the canonical terms (codes) representing them in the object theory. It is thus an operation entirely at the meta level. It is necessary to have a new sort at the meta level containing the names of codes (it is therefore a subsort of the sort containing names of terms).

Note, there cannot be a sort of codes at the object level because the codes are terms in a certain canonical form. Thus of two terms representing the same object one might be a code and the other not, but these two terms must necessarily have the same sort at the object level.

Substitution Function

OBJECT THEORY

The substitution function is a function of the object theory.

META THEORETICAL DEFINITION

The only property required of subst is that it satisfies (*). It is necessary to express this property as an axiom at the meta level.

The right hand side of (*) requires the computation of \(W[n/v]\) which is basically the substitution function for names of expressions. The function which performs this is provided by semantic attachment to a GETFOL substitution routine via the function substfree.

To state the substitution axiom it is necessary to have a name for subst.

The axiom is a direct translation of (*).

Proof

The GETFOL formalisation of the proof is interesting because it enforces a separation between the meta-theoretic and object-theoretic steps. As a matter of fact practically all the proof is performed at the meta level, because that is the only level at which the intensional equivalence (ie. same name and therefore same code) can be expressed.

OBJECT LANGUAGE

The informal proof starts with the wff \(\Psi\) (which is to be diagonalised) and a selected variable. To simplify matters the formalised proof will be given for an arbitrary unary predicate instead of a wff with one free variable.

The code of \(v_0\) exists at the object level. As the coding is purely hypothetical it is necessary to declare a constant to represent this code.

META REPRESENTATION

The meta language must have names for the alphabet of the object language.

\(\sim v_0\sim\) is defined to be the code of \(v_0\) by an axiom.

DEFINITION OF \(\Theta\)

There is no mechanism for making an abbreviating definition in GETFOL. Thus to force \(\Theta\) to be the same wff as \(\Psi(v_0,\sim v_0\sim,v_0)\) it is necessary to define the name of \(\Theta\) as equal to the name of \(\Psi(v_0,\sim v_0\sim,v_0)\). Thus \(\Theta\) is defined at the meta level.

It turns out that \(\Theta\) is not needed at the object level, however its code is.

PROOF STEPS (A) - (C)

(A) is obtained as an instance of (*) (ie. AX_subst) by doing forall elimination using "THETA", "v0" and "~THETA~", then substituting the occurrence of encodewff("THETA") with the identical "~THETA~", and the occurrence of encodevar("v0") with the identical "~v0~".

(B) is derived precisely by means of computing the substitution using the definition of \(\Theta\) and the GETFOL substitution function which is attached to substfree.

(C) follows by a simple substitution.

DEFINITION OF \(\Phi\)

\(\Phi\) is defined by a meta level axiom in the same way as \(\Theta\). This time \(\Phi\) is also required as a sentence at the object level. Note that actually \(\Phi\) already exists at the object level in its expanded form, however it is nice to make things readable ...

PROOF STEPS (D) & (E)

(D) follows from the abbreviation of \(\Phi\) in (C) and the substitution of encodewff("PHI") with the identical "~PHI~".

(E) is an instance of the trivial (A1) after substitution of identities.

DEDUCING (DIAG)

The last part of the proof is the only part at the object level. (D) and (E) are reflected into theorems at the object level. (DIAG) then follows by substitution of equals at the object level. Note this is an essentially object level step because the equality does not hold at the meta level.

(top, beg)

Playground