truthtable-js

A powerful TypeScript library for generating and validating propositional logic truth tables. Inspired by Carnap's truth table implementation, this library provides a flexible API for creating, manipulating, and validating truth tables for propositional logic formulas.

Features

• Multiple Table Types
  • Simple truth tables for propositional formulas
  • Validity tables with turnstile notation (⊨, ⊢, |-)
  • Partial truth tables for specific scenarios
    • Primarily generating blank tables for students to fill in
• Formula Support
  • Full propositional logic formula parsing (via tfl-js)
  • Support for common logical operators (∧, ∨, →, ↔, ¬)
  • Custom operator symbol configuration
• Validation Capabilities
  • Table completion validation
  • Counterexample detection for:
    • Inequivalence
    • Consistency
    • Non-contradiction
    • Invalidity
    • Non-tautology
• Customization
  • Custom truth value markers (T/F, 1/0, ⊤/⊥, etc.)
  • Configurable table formatting options
  • Extensible serialization system with schema validation

Installation

npm install truthtable-js
# or
yarn add truthtable-js
# or
bun install truthtable-js

Basic Usage

import { TFLParser } from 'tfl-js';
import { SimpleTruthTable, TableSerializer } from 'truthtable-js';

// Create a simple truth table
const parser = new TFLParser();
const formula = parser.parse('p → (q ∧ r)');
const table = new SimpleTruthTable(formula, {
  truthValues: {
    trueMarker: 'T',
    falseMarker: 'F'
  },
  showSubformulas: true,
  operatorSymbols: {
    and: '∧',
    or: '∨',
    not: '¬',
    if: '→',
    iff: '↔'
  }
});

// Get the table data
const tableData = table.toJSON();
console.log('Table Data:', tableData);

// Serialize the table data
const serializer = new TableSerializer();
const serializedData = serializer.serializeTableData(tableData);

Table Types

Simple Truth Tables

import { TFLParser } from 'tfl-js';
import { SimpleTruthTable } from 'truthtable-js';

// Create a truth table for a complex formula
const parser = new TFLParser();
const formula = parser.parse('(p → q) ∧ (q → r)');
const table = new SimpleTruthTable(formula, {
  truthValues: {
    trueMarker: '1',
    falseMarker: '0'
  },
  showSubformulas: true
});

// Get table data
const data = table.toJSON();
console.log('Atoms:', data.columns.atoms);
console.log('Formulas:', data.columns.formulas);
console.log('Rows:', data.rows);

// Validate a solution
const solution = [
  [true, true, true, true, true, true, true],
  [true, true, false, true, false, false, false],
  [true, false, true, false, true, false, false],
  [true, false, false, false, true, false, false],
  [false, true, true, true, true, true, true],
  [false, true, false, true, true, true, true],
  [false, false, true, true, true, true, true],
  [false, false, false, true, true, true, true]
];

const result = table.validate(solution);
if (!result.isValid) {
  console.log('Validation errors:', result.errors);
}

Validity Tables

import { TFLParser, parseSequent } from 'tfl-js';
import { ValidityTable } from 'truthtable-js';

// Create a validity table from premises and conclusion
const parser = new TFLParser();
const premises = [parser.parse('p → q'), parser.parse('q → r')];
const conclusion = parser.parse('p → r');
const validityTable = new ValidityTable(premises, conclusion, {
  turnstileType: 'semantic',  // 'semantic' (⊨), 'syntactic' (⊢), or 'ascii' (|-)
  isNegated: false           // false for ⊨, true for ⊭
});

// Or create from a sequent string
const table = ValidityTable.fromSequent('p → q, q → r ⊨ p → r', {
  turnstileType: 'semantic',
  isNegated: false,
  showSubformulas: true
});

// Check if the argument is valid
if (table.isValid()) {
  console.log('The argument is valid');
} else {
  // Find a counterexample
  const result = table.findCounterexample();
  if (result.exists) {
    console.log('Counterexample found:', result.valuation);
  }
}

Partial Truth Tables

import { TFLParser } from 'tfl-js';
import { PartialTruthTable } from 'truthtable-js';

// Create a partial truth table with given rows
const parser = new TFLParser();
const formula = parser.parse('p ∨ q');
const table = new PartialTruthTable([formula], {
  givenRows: [
    { p: true, q: false },
    { p: false, q: true }
  ],
  onlyGivenRows: true,
  showSubformulas: true
});

// Get table data
const data = table.toJSON();
console.log('Atoms:', data.columns.atoms);
console.log('Formulas:', data.columns.formulas);
console.log('Rows:', data.rows);

Table Generator

For more direct control over table generation:

import { TFLParser } from 'tfl-js';
import { TableGenerator } from 'truthtable-js';

// Create a parser and formula
const parser = new TFLParser();
const formula = parser.parse('(p ∧ q)');

// Create a table generator
const generator = new TableGenerator();

// Generate a simple table
const table = generator.generateSimpleTable([formula]);

// Generate a validity table
const premises = [parser.parse('p → q'), parser.parse('q → r')];
const conclusion = parser.parse('p → r');
const validityTable = generator.generateValidityTable(premises, conclusion);

Serialization

import { TableSerializer } from 'truthtable-js';

const serializer = new TableSerializer();

// Serialize table data
const tableData = serializer.serializeTableData(table.toJSON());

// Serialize validation result
const validationData = serializer.serializeValidationResult(table.validate(solution));

// Serialize counterexample result
const counterexampleData = serializer.serializeCounterexampleResult(table.findCounterexample());

// Serialize table options
const optionsData = serializer.serializeTableOptions({
  turnstileType: 'semantic',
  isNegated: false,
  truthValues: {
    trueMarker: 'T',
    falseMarker: 'F'
  },
  showSubformulas: true,
  operatorSymbols: {
    and: '∧',
    or: '∨',
    not: '¬',
    if: '→',
    iff: '↔'
  }
});

Demo Output

Here's an example of what the table generator outputs for a simple truth table:

// Example output for SimpleTruthTable with formula 'p ∧ q'
{
  "formulas": ["(p ∧ q)"],
  "atoms": ["p", "q"],
  "columns": {
    "atoms": [
      { "symbol": "p", "index": 0 },
      { "symbol": "q", "index": 1 }
    ],
    "formulas": [
      {
        "formula": "(p ∧ q)",
        "symbols": [
          { "type": "paren", "symbol": "(" },
          { "type": "atom", "symbol": "p", "index": 0 },
          { "type": "operator", "symbol": "∧", "isMainOperator": true, "index": 2 },
          { "type": "atom", "symbol": "q", "index": 1 },
          { "type": "paren", "symbol": ")" }
        ]
      }
    ]
  },
  "rows": [
    [true, true, true],
    [true, false, false],
    [false, true, false],
    [false, false, false]
  ],
  "options": {
    "turnstileType": "semantic",
    "isNegated": false,
    "truthValues": {
      "trueMarker": "T",
      "falseMarker": "F"
    },
    "showSubformulas": true,
    "operatorSymbols": {
      "and": "∧",
      "or": "∨",
      "not": "¬",
      "if": "→",
      "iff": "↔",
      "turnstile": "⊨"
    }
  }
}

And for a validity table:

// Example output for ValidityTable with premises 'p → q', 'q → r' and conclusion 'p → r'
{
  "formulas": ["(p → q)", "(q → r)", "(p → r)"],
  "atoms": ["p", "q", "r"],
  "columns": {
    "atoms": [
      { "symbol": "p", "index": 0 },
      { "symbol": "q", "index": 1 },
      { "symbol": "r", "index": 2 }
    ],
    "turnstile": {
      "symbol": "⊨",
      "index": 5
    },
    "formulas": [
      {
        "formula": "(p → q)",
        "symbols": [
          { "type": "paren", "symbol": "(" },
          { "type": "atom", "symbol": "p", "index": 0 },
          { "type": "operator", "symbol": "→", "isMainOperator": true, "index": 3 },
          { "type": "atom", "symbol": "q", "index": 1 },
          { "type": "paren", "symbol": ")" }
        ]
      },
      {
        "formula": "(q → r)",
        "symbols": [
          { "type": "paren", "symbol": "(" },
          { "type": "atom", "symbol": "q", "index": 1 },
          { "type": "operator", "symbol": "→", "isMainOperator": true, "index": 4 },
          { "type": "atom", "symbol": "r", "index": 2 },
          { "type": "paren", "symbol": ")" }
        ]
      },
      {
        "formula": "(p → r)",
        "symbols": [
          { "type": "paren", "symbol": "(" },
          { "type": "atom", "symbol": "p", "index": 0 },
          { "type": "operator", "symbol": "→", "isMainOperator": true, "index": 6 },
          { "type": "atom", "symbol": "r", "index": 2 },
          { "type": "paren", "symbol": ")" }
        ]
      }
    ]
  },
  "rows": [
    [true, true, true, true, true, true, true],
    [true, true, false, true, false, true, false],
    [true, false, true, false, true, true, true],
    [true, false, false, false, true, true, false],
    [false, true, true, true, true, true, true],
    [false, true, false, true, false, true, true],
    [false, false, true, true, true, true, true],
    [false, false, false, true, true, true, true]
  ],
  "turnstileIndex": 5,
  "premises": ["(p → q)", "(q → r)"],
  "conclusion": "(p → r)",
  "turnstile": "⊨",
  "options": {
    "turnstileType": "semantic",
    "isNegated": false,
    "truthValues": {
      "trueMarker": "T",
      "falseMarker": "F"
    },
    "showSubformulas": true,
    "operatorSymbols": {
      "and": "∧",
      "or": "∨",
      "not": "¬",
      "if": "→",
      "iff": "↔",
      "turnstile": "⊨"
    }
  }
}

License

[MIT]

Acknowledgments

This library is inspired by the Carnap project's truth table implementation, reimagined for modern JavaScript/TypeScript applications.