About the characterization of a fine line that separates generalizations and boundary-case exceptions for the Second Incompleteness Theorem under semantic tableau deduction. (30th December 2020)

• Record Type: Journal Article
• Authors: Willard, Dan E
• Is Part Of: Journal of logic and computation. Volume 31:Number 1(2021)
• Page Start: 375
• Page End: 392
• Publication Date: 2020-12-30
• Subjects: semantic tableau deduction -- Hilbert's second problem -- partial revival of Hilbert's consistency program -- generalizations of the second incompleteness theorem; Logic programming -- Periodicals; Logic, Symbolic and mathematical -- Periodicals; Computational complexity -- Periodicals; 005.115
• DOI: 10.1093/logcom/exaa083
• Languages: English
• ISSNs: 0955-792X

Abstract

Abstract: Our previous research showed that the semantic tableau deductive methodology of Fitting and Smullyan permits boundary-case exceptions to the second incompleteness theorem, if multiplication is viewed as a 3-way relation (rather than as a total function). It is known that tableau methodologies prove a schema of theorems verifying all instances of the law of the excluded middle. But if one promotes this schema of theorems into formalized logical axioms, then the meaning of the pronoun of 'I', used by our self-referencing engine, changes quite sharply. Our partial evasions of the second incompleteness theorem shall then come to a complete halt.