The Original Statement on Decidability and Formal Proof Systems

Decidability: A formal logic is decidable if it can be proven that A follows from T by a mechanistic algorithm of finite terms. A theory must have a model. A theory L is a well ordered system of at least one formula which must be true for the case to be true otherwise it is inconsistent.

We pursue a formulae in some system of sequences of formulae, within which we can define a property Is_a_proof(p) capable of being verified by an algorithm, such that we can be certain that the final component t of any sequence p satisfying Is_a_proof(p) is universally valid. Then we can use intuition freely to find aesthetically pleasing sequences p, the proofs, leading to interesting end goals t, the theorems (Schwartz).

Decidability in Formal Logic

A formal logic is decidable if there exists a mechanistic algorithm that can determine in finite time whether a given formula A follows from a theory T. For a theory to be meaningful, it must have at least one model (an interpretation where all its statements are true).

function isDecidable(theory T, formula A) { // Algorithm must terminate in finite steps // with correct answer for all inputs return true/false; // Whether T ⊢ A }

Consistent Theory

A well-ordered system of formulas where:

• At least one formula is true
• No contradictions exist
• Has at least one model

Decidable Theory

Characteristics:

• Algorithm exists for proof verification
• Always terminates
• Sound and complete

Proof Systems and Verification

Formal System (L): A language with well-formed formulas and inference rules

Proof (p): A finite sequence of formulas where each is either an axiom or follows from previous ones

Is_a_proof(p): An algorithm that verifies if p is a valid proof in L

Theorem (t): The final formula in a valid proof sequence p

Proof Verification Process

Component	Description	Computational Aspect
Formulas	Well-formed statements in the language	Syntax checking algorithm
Inference Rules	Mechanically applicable transformations	Pattern matching operations
Proof Verification	Checking each step follows from previous	Finite state automaton
Theorem Extraction	Final formula in valid proof	Terminal state detection

Intuition in Proof Discovery

While proof verification must be completely mechanistic, the discovery of proofs can leverage human intuition:

Mechanistic Verification

• Algorithmic
• Deterministic
• Finite steps

Creative Discovery

• Intuitive leaps
• Aesthetic choices
• Heuristic search

// Human-guided proof search
function findProof(goal, intuitionHeuristics) {
  while (!is_a_proof(currentAttempt)) {
    nextStep = applyIntuition(intuitionHeuristics);
    currentAttempt.append(nextStep);
  }
  return currentAttempt; // Verified proof
}

Example: Propositional Logic

Consider a simple decidable system with these properties:

Axiom Schema	Inference Rule	Decidability
φ → (ψ → φ)	Modus Ponens	Truth tables provide decision procedure

Goal: Prove (p → p)

Step 1: Instance of Axiom 1: p → ((p → p) → p)

Step 2: Instance of Axiom 2: [p → ((p → p) → p)] → [(p → (p → p)) → (p → p)]

Step 3: Apply MP to Step 1 and Step 2

Theorem: (p → p)