Frege

---

📋 Table of Contents

- Installation
- Requirements
- Installing
- Overview
- Symbols and Variables
- Parse
- Formula string to Object
- Object to Formula string
- Evaluate
- Reduce
- Truth Tables
- Print Truth Table
- Formula Properties
- isTautology
- isContingency
- isContradiction
- Check Proof
- Semantic Consequence
- Technologies
- Requirements
- Installing and configuring the project
- But why "Frege"?
- How to contribute
- License

💻 Installation

$3

- Node.js
- Yarn, NPM or similar.

$3

``bash
$ npm -i fregejs
`

👀 Overview

"Frege" is a lib created by the Boolestation Team in order to assist in tasks involving propositional logic.

Constructing formulas, simplifying them, checking semantic or syntactic validity are responsibilities that Frege proposes to resolve.

$3

When passing propositional logic formulas to some Frege function, it is necessary to know that the accepted symbols are the following:
`typescript
export type Operator = '¬' | '∧' | '∨' | '->' | '<->' | '!' | '&' | '|';
`
Parentheses ( "()" ) are also accepted.

When entering any propositional variable, only uppercase A - Z letters will be accepted.

`typescript
// Supported ✅
frege.evaluate('¬(P ∧ Q)', {P: false, Q: true});

// Not supported ❌
frege.evaluate('~(p ^ Q)', {p: false, Q: true});
`




$3

Frege allows the developer to work with object formulas or with string formulas. It is possible to carry out the conversion process mutually. Strings can be parsed to objects and objects can be parsed to strings.

#### Formula string to Object:
`typescript
import { frege } from 'fregejs';

frege.parse.toFormulaObject('P -> Q'); // {1} Implication
frege.parse.toFormulaObject('P <-> Q'); // {2} Biconditional
frege.parse.toFormulaObject('P ∧ Q'); // {3} Conjunction
frege.parse.toFormulaObject('P ∨ Q'); // {4} Disjunction
frege.parse.toFormulaObject('¬P'); // {5} Negation

/*
Alternative Symbols:
*/
frege.parse.toFormulaObject('P & Q'); // {6} Conjunction
frege.parse.toFormulaObject('P | Q'); // {7} Disjunction
frege.parse.toFormulaObject('!P'); // {8} Negation
`
output:
`typescript
{ operation: 'Implication', left: 'P', right: 'Q' } // {1} Implication
{ operation: 'Biconditional', left: 'P', right: 'Q' } // {2} Biconditional
{ operation: 'Conjunction', left: 'P', right: 'Q' } // {3} Conjunction
{ operation: 'Disjunction', left: 'P', right: 'Q' } // {4} Disjunction
{ operation: 'Negation', value: 'P' } // {5} Negation

/*
Alternative Symbols:
*/
{ operation: 'Conjunction', left: 'P', right: 'Q' } // {6} Conjunction
{ operation: 'Disjunction', left: 'P', right: 'Q' } // {7} Disjunction
{ operation: 'Negation', value: 'P' } // {8} Negation
`

#### Object to Formula string:
`typescript
frege.parse.toFormulaString({ operation: 'Implication', left: 'P', right: 'Q' }); // {1} Implication
frege.parse.toFormulaString({ operation: 'Biconditional', left: 'P', right: 'Q' }); // {2} Biconditional
frege.parse.toFormulaString({ operation: 'Conjunction', left: 'P', right: 'Q' }); // {3} Conjunction
frege.parse.toFormulaString({ operation: 'Disjunction', left: 'P', right: 'Q' }); // {4} Disjunction
frege.parse.toFormulaString({ operation: 'Negation', value: 'P' }); // {5} Negation
`
output:
`
(P -> Q) // {1}
(P <-> Q) // {2}
(P ∧ Q) // {3}
(P ∨ Q) // {4}
¬(P) // {5}
`

$3


The "evaluate" function calculates the truth value of a molecular formula according to the truth value of its atomic formulas.
`typescript
import { frege } from 'fregejs';

const first = frege.evaluate('P->(Q->P)', { P: false, Q: true }); // {1}

const second = frege.evaluate(
{
operation: 'Conjunction',
left: 'P',
right: { operation: 'Negation', value: 'P' }
},
{ P: true }
); // {2}

const third = frege.evaluate('¬¬P ∨ ¬P', { P: true }); // {3}

console.log('first:', first)
console.log('second:', second);
console.log('third:', third);
`
output:
`typescript
first: true
second: false
third: true
`


$3


The "reduce" function reduces any logical formula that uses implications or biconditionals to a logical formula that uses only the operators of: conjunction, negation and disjunction.
`typescript
import { frege } from 'fregejs';
frege.reduce('( P -> Q ) ∨ (A ∧ B)'); // {1}
frege.reduce('P <-> ( Q -> P )'); // {2}
`
output:
`
((¬(P) ∨ Q) ∨ (A ∧ B)) // {1}
((¬(P) ∨ (¬(Q) ∨ P)) ∧ (¬((¬(Q) ∨ P)) ∨ P)) // {2}
`

$3

The "generateTruthTable" function generates a truth table for the formula passed in the parameter. The returned value will be an object, which contains a header, with the propositional variables and the formula in question; the truth-value combinations for propositional variables; the truth values of the formula according to each combination.

`typescript
import { frege } from 'fregejs';

frege.generateTruthTable('P->(Q->P)'); // {1}
frege.generateTruthTable({operation: 'Conjunction', left: 'P', right: 'Q'}); // {2}
`
output:
`typescript
// {1}
{
headers: [ 'P', 'Q', 'P->(Q->P)' ],
truthCombinations: [ [ false, false ], [ false, true ], [ true, false ], [ true, true ] ],
truthValues: [ true, true, true, true ]
}

// {2}
{
headers: [ 'P', 'Q', '(P ∧ Q)' ],
truthCombinations: [ [ false, false ], [ false, true ], [ true, false ], [ true, true ] ],
truthValues: [ false, false, false, true ]
}
`
#### Print Truth Table
`typescript
import { printTruthTable, frege } from 'fregejs';

const truthTable = frege.generateTruthTable('P->Q');
printTruthTable(truthTable);
`
output:
`bash
P Q P->Q
F F T
F T T
T F F
T T T
`

$3

We can also check some properties of a formula using the "isContingency", "isTautology" or "isContradiction" functions.

#### isTautology
`typescript
const formula = 'P->(Q->P)';
const isTautology = frege.isTautology(formula);
console.log(Is "${formula}" a tautology? ${isTautology}); // Output: Is "P->(Q->P)" a tautology? true
`

#### isContingency

`typescript
const formula = 'P <-> Q';
const isContingency = frege.isContingency(formula);
console.log(Is "${formula}" a contingency? ${isContingency}); // Output: Is "P <-> Q" a contingency? true
`

#### isContradiction
`typescript
const formula = 'P ∧ ¬P';
const isContradiction = frege.isContradiction(formula);
console.log(Is "${formula}" a contradiction? ${isContradiction}); // Output: Is "P ∧ ¬P" a contradiction? true
`


$3


The "checkproof" function evaluates the validity of the logical test passed in the parameter. If it is valid, it displays the application of the rules in the console and returns true. Otherwise, it throws an InferenceException, explaining the reason for its invalidity.

`typescript
import { frege, Proof } from 'fregejs';
const { toFormulaObject } = frege.parse;

const proof: Proof = {
1: {
id: 1,
expression: toFormulaObject('¬P ∧ ¬Q'),
type: 'Premise'
},
2: {
id: 2,
expression: toFormulaObject('(P ∨ Q)'),
type: 'Hypothesis'
},

3: {
id: 3,
expression: toFormulaObject('¬P'),
from: [[1], 'Conjunction Elimination'],
type: 'Knowledge'
},
4: {
id: 4,
expression: toFormulaObject('¬Q'),
from: [[1], 'Conjunction Elimination'],
type: 'Knowledge'
},
5: {
id: 5,
expression: toFormulaObject('P'),
from: [[2, 4], 'Disjunctive Syllogism'],
type: 'Knowledge'
},
6: {
id: 6,
expression: toFormulaObject('P ∧ ¬P'),
type: 'End of Hypothesis',
hypothesisId: 2,
from: [[5, 3], 'Conjunction Introduction']
},
7: {
id: 7,
expression: toFormulaObject('(P ∨ Q) -> (P ∧ ¬P)'),
type: 'Knowledge',
from: [[2,6], 'Conditional Proof']
},
8: {
id: 8,
expression: toFormulaObject('¬(P ∨ Q)'),
type: 'Conclusion',
from: [[7], 'Reductio Ad Absurdum']
}
}

frege.checkProof(proof); // {1}
`
output:
`
Applied Conjunction Elimination with success at line 3 ✔️
Applied Conjunction Elimination with success at line 4 ✔️
Applied Disjunctive Syllogism with success at line 5 ✔️
Applied Conjunction Introduction with success at line 6 ✔️
Applied Conditional Proof with success at line 7 ✔️
Applied Reductio Ad Absurdum with success at line 8 ✔️

{ (¬(P) ∧ ¬(Q)) } ⊢ ¬((P ∨ Q))
`
Fallacy of affirming the consequent:
`typescript
const proof: Proof = {
1: {
id: 1,
expression: toFormulaObject('P -> Q'),
type: 'Premise'
},
2: {
id: 2,
expression: toFormulaObject('Q'),
type: 'Premise'
},
3: {
id: 3,
expression: toFormulaObject('P'),
type: 'Conclusion',
from: [[1, 2], 'Modus Ponens']
},
}

frege.checkProof(proof); // {2}
`

output:
`
InferenceException [Error]: Modus Ponens: cannot apply in (P -> Q) with Q
`

$3

The function "verifyConsequence.semantic" identifies if there is a case where, in a truth table, all premises are true, but the conclusion is false.

If so, it returns false. Else, returns true.
`typescript
import { frege } from 'fregejs';

const first = frege.verifyConsequence.semantic(['P->Q', 'Q'], 'P'); // {1}
const second = frege.verifyConsequence.semantic(['P->Q', 'P'], 'Q'); // {2}

console.log('first: ', first);
console.log('second: ', second);
`
output:
`
first: false
second: true
``

🚀 Technologies

The main technologies used are:

- Node.js
- TypeScript
- llang

But why Frege?

> "Friedrich Ludwig Gottlob Frege (/ˈfreɪɡə/;[[15]](https://en.wikipedia.org/wiki/Gottlob_Frege#cite_note-15) German: [[ˈɡɔtloːp ˈfreːɡə]](https://en.wikipedia.org/wiki/Help:IPA/Standard_German "Help:IPA/Standard German"); 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic philosophy, concentrating on the philosophy of language, logic, and mathematics." via Wikipedia.

🤔 How to contribute

Thanks for taking an interest in contributing. New features, bug fixes, better performance and better typing are extremely welcome.

📝 License

This project is licensed under the MIT License - see the LICENSE file for details.