[isabelle] Some corrections and amendments



Dear Andrei Popescu, dear Ramana Kumar,
dear Members of the Research Community,

As a matter of fairness, I have to correct one of my earlier statements.

Andrei Popescu correctly pointed out at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00059.html
that neither "being based on a meta-logic" (i.e., a logical framework) nor 
"featuring a natural deduction system" creates a problem.
There has been a misunderstanding on my part.
However, I have to say that Paulson's definition of the turnstile as a symbol 
for the predicate "hfthm" in
"inductive hfthm :: "fm set => fm => bool" (infixl "â" 55)"
	https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html
somewhere hidden in the proof files without being prominently announced in his 
articles is strongly misleading and inevitably creates misinterpretations. 
Usually (such as in [Andrews, 2002]), the turnstile is used to indicate the 
provability of a theorem of the logic in which the proof is undertaken, not the 
provability of theorems of the embedded logic. Also, for the predicate of 
provability of theorems of the embedded (represented, formalized) logic, a 
label is usually used, not a symbolic notation (e.g., Goedel uses "Bew" - for 
"beweisbare Formel", the German expression for "provable formula" -, and 
O'Connor in Coq uses "SysPrf"). Moreover, without some short introduction to 
the notation and the type system it is nearly impossible to analyze the proof 
in detail unless one has advanced experience with the Isabelle proof assistant, 
leaving aside that with a logical framework there are not only three, but four 
language levels involved, all of which one would ideally need to understand in 
order to verify the proof.

The result of the formal proof
    ~Bew(g) /\ ~Bew(not g)
can be interpreted in the sense that it is possible to construe a formula with 
the form of a sentence (i.e., a boolean-valued well-formed formula with no free 
variables) neither provable nor refutable.
Nevertheless, the claim of "incompleteness" depends on a philosophical 
assumption.
One who shares the semantic view (model theory) will conclude that there is a 
meaningful (and true) sentence that is neither provable nor refutable, and will 
call the discrepancy between syntax and semantics "incompleteness".
But one who shares the syntactic view will conclude that it is possible to 
create a meaningless formula which has the form of a syntactically correct 
sentence (similar, in natural language, to a grammatically correct but 
meaningless statement like "mathematics is liquid").

Concerning the two objections of Ramana Kumar at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00061.html
the first one was a misunderstanding clarified at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html
But the second, Ramana Kumar's claim that type "tm" can be defined like type 
"nat", is not correct. Andrews' logic Q0, being an improved variant of Church's 
original simple type theory, only allows the types iota (i) and omicron (o), 
and combinations of them.
Andrews' type "nat" is such a combination ( nat := (o(oi)) ). On the contrary, 
Paulson's type "tm" is an inductively defined type, which is not possible in Q0:
"nominal_datatype tm = Zero | Var name | Eats tm tm"
	https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html
In an e-mail, Paulson basically argued that there should be ways to introduce 
further types (instead of restricting oneself to combinations of 'i' and 'o'). 
This is, of course, correct, but doesn't justify the specific mode of type 
introduction used here, namely the Backus-Naur form (BNF). The BNF was designed 
to specify formal grammars in computer science, but (mathematical) types are 
objects that must have certain logical properties, such as being non-empty. 
Thus the introduction of additional mathematical types should be subject to 
proof, and not a matter of mere declaration via the BNF.

With some more knowledge about the concept of the current proof assistants, I 
can answer Ramana Kumar's question at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00149.html
concerning the motivation of my project announcement at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html
from his perspective now.
Current proof assistants seem to follow the semantic approach, in which the 
theory is distinguished from a specific linguistic (formal) formulation, or use 
of model theoretic notions like satisfiability is made. For example, in 
Isabelle there are implementations of both axiomatic set theory (Isabelle/ZF) 
and type theory (Isabelle/HOL), but neither one is explicitly preferred, and 
the question of which is more adequate for representing mathematics is not even 
raised. (Although, unlike in informal mathematics, in formalized proofs type 
theory seems to prevail, e.g., within Isabelle the logic Isabelle/HOL, a 
polymorphic version of Church's simple type theory.)
If one follows the syntactic approach, then there is a desire for something 
like the ideal formulation or the natural language of formal logic and 
mathematics. The main criterion is expressiveness [cf. Andrews, 2002, p. 205], 
or, vice versa, the reducibility of mathematics to a minimal set of primitive 
rules and symbols. If we leave away for a moment the restrictions of Q0 of 
still being a formulation of simple type theory (i.e., without type variables 
and dependent types), all of formal logic and mathematics can be expressed on 
the basis of only a "single rule of inference (substitution, from which the 
rule of modus ponens is derived)" and "only two basic types (individuals and 
truth values) and only two basic constants (identity/equality and its 
counterpart, description)"
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html
Paulson argued that natural deduction is far superior to Hilbert-style systems 
for automated proof. This is, of course, correct, since Hilbert-style 
metatheorems become symbolically representable in natural deduction as regular 
theorems (and not just metatheorems), but this only reflects the engineer's 
perspective with the pragmatic aim of quickly obtaining proofs. For the 
philosopher it is not proof automation but expressiveness that is the main 
criterion, such that the method with the least amount of rules of inferences, 
i.e., a Hilbert-style system, is preferred, and all other rules become derived 
rules.
Hence, from the perspective of the syntactic view, Andrews' elegant logic Q0 is 
the natural point to start with. Overcoming its restrictions by extending it to 
a polymorphic (with type variables) and dependent type theory (with dependent 
types) is the motivation of my logic R0, which I hope to be able to publish 
soon. A preliminary excerpt with some definitions and a sample proof is 
available online at
	http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf

Kind regards,

Ken Kubota

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.