New Logic Project

Tableau-Looper - FOL-Resolver - FOL-Decider - FOL-ModelCheck - FOL-Optimizer - FOL-Skolemizer - KromHornSolver - PL-Decider - Q-Decider - Kronecker-Decider - Finitismus

New Logic is an algorithmic conception of first-order logic influenced by Wittgenstein's philosophy and his critique of Mathematical Logic.
Its main idea is to decide logical properties (such as provability, consistency, satisfiability) by detection of patterns in normal forms or proof search sequences.
According to this idea, the conception of logic is not only algorithmic but also iconic.
The details of this approach are spelled out in my publications and the software available via this site:

Iconic Proof Conception:

Decidability and Notation, Logique et Analyse 251 (2020), pp. 365-386.

Iconic Proofs and First-Order Logic:

Iconic Logic and Ideal Diagrams: The Wittgensteinian Approach.Diagrammatic Representation and Inference (2018), pp. 624-639.
Wittgenstein's ab-notation: An Iconic Proof Procedure, History and Philosophy of Logic 38.3 (2017), pp. 239-262.
PL-Decider: software for ab-notation in propositional logic.
Wittgenstein's Conjecture, Proceedings of the 41st International Ludwig Wittgenstein-Symposium in Kirchberg (2018), pp. 515-534.
Wittgenstein's Elimination of Identity for Quantifier-Free Logic (with Markus S�bel) The Review of Symbolic Logic 14.1, pp. 1-21.
FOL-Optimizer: software for converting pure FOL-formulas to optimized distributive normal forms.Minimizing Disjunctive Normal Forms of Pure First-Order Logic, Logic Journal of the IGPL 25.3 (2017), pp. 325-347.
FOL-Decider: software for proof search in first-order logic via the NNF-calculus. A Decision Procedure for Herbrand Formulas without Skolemization, pp. 1-30., FOL-Decider, pp. 1-43.
FOL-Model Checker: software for generating models for pure FOL formulas.
Tableau-Looper: a 3-value decider for disproof, satisfiability, and Looping based on tableaux with clauses.
FOL-Resolver: a 3-value decider for disproof, satisfiability, and Looping based on resolution with clauses.
Wittgenstein and G�del: An Attempt to make `Wittgenstein's Objection' reasonable, Philosophia Mathematica 25.3, pp. 324-345.
Critique of the Church-Turing Theorem.

Iconic Proofs and Mathematical Proofs:

Q-Decider: software for an iconic decision procedure of equations with rational numbers.
Kronecker-Decider: software for deciding upon the dimensions of polynomials.
Wittgenstein on the Infinity of Primes, History and Philosophy of Logic 29 (2008), pp. 63-81.
Wittgenstein on Pseudo-Irrationals, Diagonal Numbers and Decidability, The Logica Yearbook 2008, pp. 95-111.

Iconic Proofs and Experimental Proofs:

Newton's Experimental Proofs: , Theoria, An International Journal for Theory, History and Foundations of Science 36.2 (2021), pp. 261-283.
Underdetermination and Provability, British Journal for the History of Philosophy 25.2 (2017), pp. 389-400.

The following papers, however, explains why an iconic conception of logical proof is limited:

The given explanation does not apply the proof techniques of Mathematical Logic.
So, the result of the New Logic Project is that an iconic understanding of logic (or even mathematics) cannot overcome the limits of decidability.
Mathematical Logic is right and the more powerful account.
One might conceive the iconic understanding of logic (and mathematics) as a conception of "primitive" logic (and "primitive" school mathematics) that is, though limited, beautiful according to its own aesthetic and philosophical standards.

Datenschutzerklaerung