New Logic: First-Order Logic from an Algorithmic Point of View

New Logic is an algorithmic conception of first-order logic influenced by Wittgenstein's philosophy and his critique of Mathematical Logic. The upshot of the Wittgensteinian view on logic is his conjecture that first-order logic (FOL) is decidable. He stuck to this conjecture even after he was confronted with Turing's proof, cf. Wittgenstein's Conjecture. This rejection of the well-established Church-Turing theorem is the main reason why a Wittgensteinian view of logic is thought to be erroneous. The New Logic Project intends to engage in a new discussion of the decision problem. Contrary to Wittgenstein, the New Logic Project (i) defines a decision procedure for FOL, the FOL-Decider, that Wittgenstein merely conjectured, (ii) provides a detailed critique of the Church-Turing Theorem, and (iii) elaborates a modest version of Wittgensteinian finitism as the systematic framework for doing logic and mathematics from an algorithmic point of view, cf. for more details. You can find an overview of my complete argument here.

The FOL-Decider rests on computing disjunctive normal forms within FOL (FOLDNFs). The basic idea of FOL-Decider is to make use of the syntax of FOLDNFs to identify either proofs of contradiction or to apply criteria for satisfiability within a finite search tree that seeks to find a proof of contradiction within a minimal number of steps (more precisely a minimal number of applying the rule of conjunction introduction A <=> A & A, the only applied rule that essentially raises complexity in the applied calculus, which I call the NNF-calculus). The algorithm of the FOL-Decider is based on nothing but well-know logical equivalence rules. The important difference to traditional proof-search calculi is the way these rules are utilized to yield expressions that allow one to apply syntactic criteria of satisfiability or contradiction. The algorithm either terminates if sufficient syntactic criteria of satisfiability can be applied or a proof of contradiction is found. In this latter case, the FOL-Decider returns an FOLDNF that is equivalent with the input-formula; and for each disjunct of that FOLDNF (i) a set of "kpairs", i.e. pairs that result in explicit contradictions if universal quantified x-variables are substituted by existential quantified y-variables and that determine a proof of contradiction, (ii) a substitution list that dictates which universal quantified x-variables are to be substituted by what kind of existential quantified y-variables, and (iii) a prenex in terms of a list of x- and y-variables that can easily be yield by applying PN-rules to the respective disjunct and that satisfies the condition that each y-variable that substitutes an x-variable according to (ii) is left to the respective x-variable. Thus, in case of contradiction, FOL-Decider finds an efficient proof that is easy to grasp once one is familiar with the proof strategies. My paper A Decision Procedure for Herbrand Formulas without Skolemization exemplifies some of the basic proof strategies of my algorithm if applied to the uncontroversial decidable fragment of Herbrand Formulas. The paper A Decision Procedure for pure First-order Logic explains and proves the procedure for the whole realm of FOL.

On the basis of the FOL-Decider, the tool ModelCheck returns a model if there is any. In the case of infinite models, a finite series of finite "transcendent" models is returned that converges to an infinite model as its limit by increasing the upper bound of the domain just as a series of decimal or rational numbers converges to a number as its limit. I call a finite model "transcendent" if its interpretations of predicates refer to some object that is not part of the finite domain of that model. In fact, this "transcendent object" will be a natural number i+1 and the finite domain of the model the series of natural numbers 1 to i. To be sure, this tool is not essential to the project of New Logic as there is no need to refer to models within this paradigm. However, as long as models remain within the realm of what is countable, computable and constructible from a finite formula, such models are acceptable according to the standards of New Logic. Thus, this tool intends to validate the assumption that any satisfiable formula has a computable model in terms of either a finite model or a model as limiting case of a series of transcendent models. If this assumption turns out to be correct, there is no need to refer to uncomputable models within the realm of FOL.

Finally, within the paradigm of New Logic, the question of specifying some equivalent to the QuineMcCluskey algorithm for FOL is prominent. You can find more about the question of optimizing FOLDNFs in my paper Minimizing Disjunctive Normal Forms of Pure First-Order Logic. A powerful tool for optimizing DNFFOLs is FOL-Optimizer. However, this tool does not satisfy the standard of identifying some DNFFOL of minimum length to its full extent. It is independent of the FOL-Decider and the question of decidability. It does not decide whether a formula is a contradiction or not but uses rather complex strategies to minimize FOLDNFs. Thus, evaluation takes quite long in intricate cases of considerable complexity. Yet, FOL-Optimizer is a convenient tool for understanding logic within the paradigm of New Logic. This is so because New Logic intends to explain logical properties on the basis of nothing but pure equivalence transformation within the formalism itself. After all, this and not set-theory, model-theory or any sort of semantics that all go beyond pure logic seems to me the most suitable standard for judgments about logical truth.

You can find some basics of this understanding of logic and its underlying iconic conception of proof in my papers Wittgenstein's ab-notation: An Iconic Proof Procedure, Iconic Logic and Ideal Diagrams: The Wittgensteinian Approach, and Decidability and Notation.

If you are interested in identity and the problems and questions that arise in extending the project of New Logic to first-order logic with identity you might consult Wittgenstein's Elimination of Identity for Quantifier-Free Logic (with Markus Säbel, forthcoming in Review of Symbolic Logic 2020).
If you are interested in the topic of deciding infinity axiom sets yuo might consult Deciding Simple Infinity Axiom Sets with OneBinary Relation by Means of Superpostulates (with Anderson Nakano, forthcoming in Proceedings of IJCAR 2020).

Powered by webMathematica


© Timm Lampert / 2019-31-07