[FOM] Formal Math Without Types?

[Mario Carneiro]

On Tue, Feb 23, 2016 at 1:04 AM, Harvey Friedman <hmflogic at gmail.com> wrote:

> I gather that in the MetaMath approach, there are variables over wffs.
> In the relatively purist approach I am talking about, I do not allow
> variables over wffs. I can see the reason for this. But for Semantic
> Representation, the case is not compelling. Also I will argue (later)
> that one can reasonably avoid this also when proofs are involved.
>

I will say a bit on how well Metamath can accommodate this viewpoint. In
your example ZFC formalism, you use terms like "phi is a formula" and one
of the definitions even uses a formula variable:

AXIOM 6 .  x1 ∈ {t: φ} ↔ (∃x2,..., x(k+1)) (φ ∧ x1 = t). Here t is a term,
φ is a formula, x1 is not in t, φ, and the free variables in t are x2,...,
x(k+1).

Since none of this stuff comes built into Metamath (all the logic and
syntax is specified via axioms), wffs and wff variables are used to
construct the recursive definition of a formula and use them in axioms such
as this. Thus to a degree you can't get away from the use of such
variables, and the system will be able to prove some theorems that use
explicit formula variables, such as |- (phi -> phi), not just instances of
this rule.

However, there is a coherent mechanism for avoiding this, which is simply
to ignore all formulas that contain wff variables. You will still need some
theorems with wff variables for the underlying propositional calculus, but
they will only be used to map wff-variable-free formulas to more
wff-variable-free formulas, and the desired subset of provable formulas
comes out, where the wff-variable-containing formulas act as schemes over
the wff-variable-free part.

I will grant that much of the necessity for having such variables goes away
if one is not interested in proofs, but only axioms. Nevertheless, there is
still a need for such variables; to define (phi /\ psi) <-> ~ (phi -> ~
psi) requires a "definition scheme" over wff variables, as does (x in {x |
phi} <-> phi).

Propositional calculus especially is the realm of wff variables, and not
having them basically means that you can't write theorems in prop calc,
which makes many proofs much longer unless you have a very complicated
axiom system for prop calc.

On Fri, Feb 26, 2016 at 6:36 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> Isabelle implements a logical framework in which there can be variables
> over any syntactic category, but they do not have the same status as
> variables in the embedded calculus (first-order logic in the case of ZF).
> This makes it possible to express the axiom scheme of separation, for
> example, as a single assertion, without extending the class of formulas
> that can be used for separation. Then entire developments can be schematic
> in such parameters. In particular, reasoning about classes can be done in a
> fairly natural way, but not allowing quantification over classes or even
> writing something like V = V.
>

I believe this stance perfectly matches Metamath's. Variables are available
for every syntactic category, but only set variables can be used in
quantifiers, so quantification over classes is not allowed (unless of
course more axioms are added to allow this). Entire developments are
schematic over these variables, and reasoning about classes is direct.
However, V = V can be written, and proven, as a special case of the scheme
A = A for a class variable A.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160226/50fae140/attachment-0001.html>