[FOM] Foundational Challenge

[Frédéric Blanqui]

Hello. You may be interested by the following paper:

Burel G. (2007) Unbounded Proof-Length Speed-Up in Deduction Modulo. In: 
Duparc J., Henzinger T.A. (eds) Computer Science Logic. CSL 2007. 
Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg

https://doi.org/10.1007/978-3-540-74915-8_37

Abstract:

In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37 years 
before: there exist arithmetical formulæ that are provable in first 
order arithmetic, but whose shorter proof in second order arithmetic is 
arbitrarily smaller than any proof in first order. On the other hand, 
resolution for higher order logic can be simulated step by step in a 
first order narrowing and resolution method based on deduction modulo, 
whose paradigm is to separate deduction and computation to make proofs 
clearer and shorter.

We prove that i + 1-th order arithmetic can be linearly simulated into 
i-th order arithmetic modulo some confluent and terminating rewrite 
system. We also show that there exists a speed-up between i-th order 
arithmetic modulo this system and i-th order arithmetic without modulo. 
All this allows us to prove that the speed-up conjectured by Gödel does 
not come from the deductive part of the proofs, but can be expressed as 
simple computation, therefore justifying the use of deduction modulo as 
an efficient first order setting simulating higher order.


Le 16/01/2020 à 08:39, Mario Carneiro a écrit :

>
>
> On Wed, Jan 15, 2020 at 7:21 PM Emilio Jesús Gallego Arias 
> <e+fom at x80.org <mailto:e%2Bfom at x80.org>> wrote:
>
>     Joe Shipman <joeshipman at aol.com <mailto:joeshipman at aol.com>> writes:
>
>     > In the case of the 4-color theorem it is the same as with other
>     computer proofs. There are 3 parts:
>     >
>     > 1) an ordinary humanly verifiable proof that an algorithm is
>     correct, translated into formalized ZFC or whatever other system
>     in the usual way,
>     > 2) the input to the algorithm (in this case, an unavoidable set
>     of reducible configurations, generated by earlier iterative
>     man-machine interaction), and
>     > 3) the trace of the algorithm (proof it halts successfully
>     obtained by
>     > actually running the computation and translating its state into the
>     > formal system’s representation; in this case, the reduction-finding
>     > subroutine for each reducible configuration can itself emit a
>     smaller
>     > more easily verified piece representing the particular reductions
>     > found).
>
>     Precisely, the Coq proof doesn't need step 3, as the algorithms are
>     written (and verified) in Coq itself. The only witness you need is the
>     output, not the trace.
>
>
>     > The paper you reference builds a lot of its own infrastructure
>     for the
>     > special purpose of this proof. But there is no particular
>     disadvantage
>     > in using a ZFC-based system to prove a statement of the form
>     > “algorithm X on input Y halts with output Z” compared with other
>     > formal systems, once the once-and-for-all work to represent
>     algorithms
>     > conveniently has been done.
>
>     My point indeed is "ZFC" cannot _run_ computation, other foundational
>     systems can; isn't this a fundamental advantage in some cases ?
>
>
> CIC is an axiomatic system that contains, among its axioms, some rules 
> about definitional equality, that we often call a "computational 
> interpretation". It so happens that these axioms can be chained 
> together in a very straightforward and deterministic way, such that a 
> "type checker" can quickly put together these proofs (implicitly, by 
> going through certain machine states).
>
> When put in these terms, it should be clear that ZFC is in a similar 
> position. If you work only from the axioms you probably won't get far, 
> but assuming that the formal system has the capability to construct 
> and reuse theorems, you can play a similar trick: use the states of a 
> computer program to quickly construct proofs of a certain form. The 
> difference is that ZFC does not specify what this form should be; this 
> depends on the implementation.
>
> As a simple example, we can do some natural number arithmetic like so:
>
> (1) 0 in nat
> (2) n in nat -> S(n) in nat
> (3) a in nat -> a + 0 = a
> (4) a, b in nat -> a + S(b) = S(a + b)
> These are all theorems of ZFC, where 0, S, and nat are ZFC sets. Now 
> we can prove
>
> S(S(0)) + S(S(0)) = S(S(S(S(0))))
>
> through an entirely algorithmic process that applies axioms (3) and 
> (4) using transitivity. We can either construct this as a concrete 
> proof object and observe that it is a valid ZFC proof, or we can write 
> a program that adds numbers in unary by pattern matching the second 
> argument, and argue that each step corresponds to an application of 
> (3) or (4), and hence each state the machine steps through implicitly 
> represents a proof in ZFC. (In this and most other cases we can also 
> prove correctness once and for all for the program, but this is a 
> slightly different thing, and the CIC analogue is closer to the sense 
> in which each intermediate state corresponds to a proof.)
>
> So to my mind there is nothing particularly special about CIC's 
> "computational interpretation", and no need whatsoever to bake this 
> into the logic. If anything, it is limiting, because it means you can 
> only compute things in one way, whereas ZFC makes no particular 
> commitment to one kind of computation; the abstract logic says nothing 
> about what is computable but computation models can be overlaid 
> without difficulty.
>
> This is essentially the way that Isabelle's code generation works; 
> although simple type theory can be argued to have a "computational 
> interpretation" as well, it is not baked into the logic in the same 
> way (there is no convertibility judgment), and Isabelle constructs 
> proof terms when you execute functions in the logic.
>
> Mario Carneiro
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200116/5d58ab33/attachment-0001.html>