Fitch-JS

We are not affiliated with the Open Logic Project or Carnap in any way. (Currently)

This is a JavaScript library for validating Fitch-style natural deduction proofs. It provides functionality to check the validity of logical proofs in both propositional and first-order logic entirely in the browser, with no server-side dependencies.

If you're familiar with Carnap or Logic Penguin, you understand what we're broadly working towards.

However, unlike these platforms (which pass the proof to a server for validation), Fitch-JS is designed to be a standalone library that can be integrated into any JavaScript application. This means you can:

• Build your own proof interface without being tied to a specific UI implementation
• Run proof validation entirely client-side with no network latency
• Use it in offline-capable web apps
• Integrate it into desktop applications via frameworks like Electron
• Include it in educational software and interactive textbooks (scorm, xapi, etc.)

Want to see a demo in action? Check out Axiom ILE (Integrated Logic Environment)!

The idea is by seperating the validator into a mini language-server, we can build a rich ecosystem of tools that can be used to build proof interfaces, homework checkers, etc.

Our goal for project "Completeness" is to support the full set of logical rules and validation requirements as presented in forall x Calgary as solved by fitch-checker.

This project is in very early Alpha. Many things may not be working the way they're expected to.

Redbull Consumed in the name of Glorious Progress: 4 Redbull.

What won't be worked on

I'm currently not interested in adding support for any proof formats than Fitch-style natural deduction as presented in forall x Calgary.

Implementation Comparison

This JavaScript implementation is a modern reimplementation of the original PHP version from fitch-checker. Both implementations support the same set of logical rules and validation requirements, ensuring a degree of compatibility and consistent behavior.

I would like to personally thank Professor Kevin C. Klement (frabjous) for the original implementation, which was the inspiration for this project.

Supported Rules

Both implementations support the full set of propositional and first-order logic rules:

Propositional Logic Rules

• Conjunction (∧I, ∧E)
• Disjunction (∨I, ∨E)
• Implication (→I, →E)
• Biconditional (↔I, ↔E)
• Negation (¬I, ¬E)
• Contradiction (⊥I, ⊥E)
• Derived Rules (DS, MT, DNE, DeM)
• Structural Rules (Pr, Hyp, R)
• Meta Rules (TND, LEM, IP)

First-Order Logic Rules

• Universal Quantification (∀I, ∀E)
• Existential Quantification (∃I, ∃E)
• Identity (=I, =E)
• Classical Quantifier (CQ)

Key Differences

1. Code Structure

   • PHP: Single file implementation with procedural style
   • JS: Modular architecture with separate modules for parsing, types, and validation

2. Type System

   • PHP: Runtime type checking with basic object types
   • JS: TypeScript-style type annotations with comprehensive interfaces

3. Validation Approach

   • PHP: Direct formula comparison with recursive checks
   • JS: Structured validation pipeline with clear separation of concerns

4. Error Handling

   • PHP: Basic error messages with line numbers
   • JS: Detailed error reporting with specific rule violation explanations

5. Testing

   • PHP: Implicit testing through usage (everything does work)
   • JS: Comprehensive test suite with unit tests and edge cases

Project Status

In Progress

• [ ] Rule validation implementations:
  • [ ] Identity Rules
    • [ ] Identity Introduction (=I)
    • [ ] Identity Elimination (=E)
    • [ ] Term substitution for identity logic
  • [ ] Classical Quantifier (CQ) rule
    • [ ] Quantifier conversion validation
    • [ ] Support for CQ rule application
  • [ ] Derived Rules
    • [ ] Double Negation Elimination (DNE)
    • [ ] Modus Tollens (MT)
    • [ ] De Morgan's Laws (DeM)
    • [ ] Disjunctive Syllogism (DS)

Completed

• [x] Project structure setup
• [x] Basic types and interfaces
• [x] Formula parsing
• [x] Core validation logic for formulas
• [x] Support for First-Order Logic operations
  • [x] Universal Elimination (∀E)
  • [x] Existential Introduction (∃I)
  • [x] Existential Elimination (∃E)
  • [x] Formula substitution
  • [x] Free variable checking
  • [x] Witness restrictions for ∃E
  • [x] Propositional Logic Rules
  • [x] Conjunction Introduction (∧I)
  • [x] Conjunction Elimination (∧E)
  • [x] Disjunction Introduction (∨I)
  • [x] Disjunction Elimination (∨E)
  • [x] Conditional Introduction (→I)
  • [x] Conditional Elimination (→E)
  • [x] Biconditional Introduction (↔I)
  • [x] Biconditional Elimination (↔E)
  • [x] Negation Introduction (¬I)
  • [x] Negation Elimination (¬E)
  • [x] Contradiction Introduction (⊥I)
  • [x] Contradiction Elimination (⊥E)
  • [x] Law of Excluded Middle (LEM)

Needed Improvements

• [ ] Additional test cases:
  • [ ] Complex nested quantifiers
  • [ ] Multiple existential eliminations
  • [ ] Invalid witness usage in conclusion
  • [ ] Subproof scope violations
  • [ ] Edge cases for variable binding
• [ ] Validation enhancements:
  • [ ] Better error messages
  • [ ] Detailed explanation of rule violations
  • [ ] Suggestions for fixing invalid proofs?
• [ ] Documentation:
  • [ ] Rule descriptions and examples
  • [ ] Common pitfalls
  • [ ] Best practices for proof construction

Project Structure

fitch-js/
├── src/
│   ├── parser.js       # Formula parsing
│   ├── types.js        # Type definitions
│   ├── rules/          # Rule implementations
│   └── proofChecker.js # Main proof checking logic
├── test/
│   ├── parser.test.js
│   ├── rules.test.js
│   └── proofChecker.test.js
└── package.json

Installation

npm install fitch-js

Or with yarn:

yarn add fitch-js

Usage

// ESM
import { parseFormula, checkProof, parseProofText } from 'fitch-js';

// CommonJS
const { parseFormula, checkProof, parseProofText } = require('fitch-js');

// Example: Existential Elimination
const proof = {
  lines: [
    {
      lineNum: 1,
      formula: parseFormula('∃x(P(x))'),
      rule: 'Pr',
      citations: [],
      subproofs: [],
      issues: []
    },
    {
      lineNum: 2,
      formula: parseFormula('Q'),
      rule: 'Pr',
      citations: [],
      subproofs: [],
      issues: []
    },
    {
      lineNum: 3,
      formula: parseFormula('P(c)'),
      rule: 'Hyp',
      citations: [],
      subproofs: [],
      issues: [],
      location: [0, 0]
    },
    {
      lineNum: 4,
      formula: parseFormula('Q'),
      rule: 'R',
      citations: [2],
      subproofs: [],
      issues: [],
      location: [0, 0]
    },
    {
      lineNum: 5,
      formula: parseFormula('Q'),
      rule: '∃E',
      citations: [1],
      subproofs: [{start: 3, end: 4}],
      issues: [],
      location: [0]
    }
  ],
  numPremises: 2,
  conclusion: parseFormula('Q')
};

const result = checkProof(proof);
console.log(result);
// {
//   isValid: true,
//   issues: [],
//   conclusionReached: true
// }

Rule Implementations

First-Order Logic Rules

Existential Elimination (∃E)

From ∃x(P(x)), to prove Q:

1. Assume P(c) for a fresh constant c
2. Derive Q without using c in premises/conclusion
3. Conclude Q by ∃E

Restrictions:

• Witness term c must not appear in:
  • Available premises
  • The conclusion Q
  • The original existential formula
• Subproof must start with assumption P(c)
• Q must be derivable from the subproof

Development

1. Clone the repository
2. Install dependencies:

   npm install

3. Run tests:

   npm test

4. Build:

   npm run build

Contributing

Contributions are welcome! Please feel free to submit a Pull Request. Before contributing:

1. Ensure all tests pass
2. Add tests for new features
3. Update documentation
4. Follow existing code style

Implemented Rules and Usage

The following rules have been fully implemented and tested. Each rule follows specific patterns and requirements:

Propositional Logic Rules

Conjunction (∧)

• Conjunction Introduction (∧I)

  • Requires two premises P and Q
  • Concludes P ∧ Q
  • Example: From P, Q derive P ∧ Q

• Conjunction Elimination (∧E)

  • Requires one premise P ∧ Q
  • Can conclude either P or Q
  • Example: From P ∧ Q derive P (or Q)

Disjunction (∨)

• Disjunction Introduction (∨I)

  • Requires one premise P
  • Can conclude P ∨ Q (or Q ∨ P) for any Q
  • Example: From P derive P ∨ Q

• Disjunction Elimination (∨E)

  • Requires a disjunction P ∨ Q and two subproofs
  • First subproof assumes P and derives R
  • Second subproof assumes Q and derives R
  • Concludes R
  • Example: From P ∨ Q, [P ⊢ R], [Q ⊢ R] derive R

Conditional (→)

• Conditional Introduction (→I)

  • Requires one subproof
  • Subproof assumes P and derives Q
  • Concludes P → Q
  • Example: From [P ⊢ Q] derive P → Q

• Conditional Elimination (→E)

  • Requires two premises: P → Q and P
  • Concludes Q
  • Example: From P → Q, P derive Q

Biconditional (↔)

• Biconditional Introduction (↔I)

  • Requires two subproofs
  • First subproof: P ⊢ Q
  • Second subproof: Q ⊢ P
  • Concludes P ↔ Q
  • Example: From [P ⊢ Q], [Q ⊢ P] derive P ↔ Q

• Biconditional Elimination (↔E)

  • Requires two premises: P ↔ Q and either P or Q
  • Concludes the other side of the biconditional
  • Example: From P ↔ Q, P derive Q (or from P ↔ Q, Q derive P)

Negation (¬)

• Negation Introduction (¬I)

  • Requires one subproof
  • Subproof assumes P and derives a contradiction (⊥)
  • Concludes ¬P
  • Example: From [P ⊢ ⊥] derive ¬P

• Negation Elimination (¬E)

  • Requires two premises: P and ¬P
  • Concludes a contradiction (⊥)
  • Example: From P, ¬P derive ⊥

Contradiction (⊥)

• Contradiction Introduction (⊥I)

  • Requires two premises: P and ¬P
  • Concludes ⊥
  • Example: From P, ¬P derive ⊥

• Contradiction Elimination (⊥E)

  • Requires one premise: ⊥
  • Can conclude any formula P
  • Example: From ⊥ derive P

Meta Rules

• Law of Excluded Middle (LEM)
  • Requires two subproofs
  • First subproof assumes P and derives R
  • Second subproof assumes ¬P and derives R
  • Concludes R
  • Example: From [P ⊢ R], [¬P ⊢ R] derive R

Structural Rules

• Reiteration (R)
  • Requires one premise P
  • Concludes P
  • Can only reiterate from available scope
  • Example: From P derive P

First-Order Logic Rules

Universal Quantification (∀)

• Universal Elimination (∀E)
  • Requires one premise ∀x(P(x))
  • Concludes P(t) for any term t
  • Example: From ∀x(P(x)) derive P(a)

Existential Quantification (∃)

• Existential Introduction (∃I)

  • Requires one premise P(t)
  • Concludes ∃x(P(x))
  • Example: From P(a) derive ∃x(P(x))

• Existential Elimination (∃E)

  • Requires one premise ∃x(P(x)) and one subproof
  • Subproof assumes P(c) for a fresh constant c and derives Q
  • Constant c must not appear in:
    • Available premises
    • The conclusion Q
    • The original existential formula
  • Concludes Q
  • Example: From ∃x(P(x)), [P(c) ⊢ Q] derive Q

Rule Requirements

Each rule has specific citation and subproof requirements:

1. Citations must reference available lines (within scope)
2. Subproofs must begin with hypotheses
3. Subproof assumptions and conclusions must match rule requirements
4. Fresh constants in ∃E must satisfy witness restrictions
5. Formulas must exactly match rule patterns

Example Valid Proofs

Here's a simple example of a valid proof using conjunction and conditional rules:

1. P         Pr
2. Q         Pr
3. P ∧ Q     ∧I 1,2
4. Q ∧ P     ∧I 2,1
5. (P ∧ Q) → (Q ∧ P)  →I [3,4]

For more examples, refer to the test file which contains numerous test cases demonstrating correct usage of each rule.