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).
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
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
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 |
