[SystemSafety] Faults in maths proofs

[Peter Bernard Ladkin]

On 2021-01-03 12:11 , David MENTRÉ wrote:
> 
> There are two commonly used definitions for a "proof-checker":
> 
>  1. The simplest program to check a proof using only the axioms of the logic. 

What if the only axiom of your logic is A |- A ?

That means, according to your definition, that all natural-deduction or reverse-natural-deduction or 
sequent calculus proof checkers fall under your definition 2.

That is not exactly helpful if what you are trying to do is classify the combinatorial complexity of 
proof checkers.

>  2. An automated prover which, as Ladkin said can used arbitrarily complicated decision procedures
>     and thus is far form being free of bugs. 

That does not follow, by any means. In particular, it does not follow because you are (arbitrarily, 
I would suggest) assigning any non-Hilbert-Bernays proof checkers to Class 2.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
ClaireTheWhiteRabbit RIP
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20210103/0cf30531/attachment.sig>