This library provides a semantically accurate implementation of first-order logic (FOL) in JavaScript. It aims to closely replicate the standard set-theoretic formulation of FOL.
This library aims to implement all primary concepts found within the standard definition of FOL.
| Concept | Implementation |
|---|---|
| First Order Language | FirstOrderLanguage(constantSymbols, variableSymbols, functionSymbols, predicateSymbols), FirstOrderParser(firstOrderLanguage) |
| First Order Structure | FirstOrderStructure(firstOrderLanguage, domain, constantsMap, functionsMap, predicatesMap) |
| Interpretation Function | FirstOrderStructure.interpret(symbol) |
| Domain Of Discourse | FirstOrderStructure.domain |
| Variable Binding | FirstOrderAssignment(?variableMap) |
| Formula Evaluation | FirstOrderEvaluator(firstOrderStructure, ?firstOrderAssignment) |
In this example we create a first-order model for modulo-10 arithmetic.
// The domain of discourse.
const domain = new Set([0, 1, 2, 3, 4, 5, 6, 7, 8, 9])
// Variables.
const variables = ['x', 'y', 'z', 'a', 'b', 'c']
// Mapping between constant symbols and their interpretations.
const constantsMap = {
0: 0,
1: 1,
2: 2,
3: 3,
4: 4,
5: 5,
6: 6,
7: 7,
8: 8,
9: 9
}
// Mapping between function symbols and their interpretations.
function mod10(n) {
return ((n % 10) + 10) % 10
}
const functionsMap = {
// Addition.
F(x, y) {
return mod10(x + y)
},
// Subtraction.
G(x, y) {
return mod10(x - y)
},
// Successor relation.
S(x) {
return mod10(x + 1)
},
// Predecessor
P(x) {
return mod10(x - 1)
},
// Additive inverse.
I(x) {
return mod10(-x)
}
}
// Mapping between predicates and their interpretations.
const predicatesMap = {
// Equality in the domain.
M(x, y) {
return x === y
},
// Less-than relation.
L(x, y) {
return x < y
}
}
// Create the first-order model.
const model = new FirstOrderLogic(
domain,
variables,
constantsMap,
functionsMap,
predicatesMap
)For all x, there is a y such that y is the successor of x. This should be true.
model.evaluate('AxEyM(y,S(x))') // trueThere is no smallest x. This should be false.
model.evaluate('-ExAy(-M(x,y)>L(x,y))') // falseThe successor of the predecessor of x is equal to x. This should be true.
model.evaluate('AxM(S(P(x)),x)') // trueThe successor of the largest element of the domain is the smallest element of the domain. This should be true.
model.evaluate('ExEy((Az(-M(x,y)>L(x,z))^Az(-M(y,z)>L(z,y)))>M(S(y),x))') // trueThere is an element which when summed with its additive inverse, results in 1. This should be false.
model.evaluate('ExM(1,F(x,I(x)))') // falseAny element summed with its additive inverse results in 0. This should be true.
model.evaluate('AxM(0,F(x,I(x)))') // trueThere is an element which is its own additive inverse. This should be true, namely on x=0 and x=5.
model.evaluate('ExM(x,I(x))') // trueIn this implementation, quantifiers are evaluated by iterating over the domain. Hence, nesting quantifiers leads to nested iteration and therefore a significant increase in evaluation time. If you have three layers of quantification for example, the evaluation time is at worst cubic in the size of the domain.
- Add support for multicharacter predicate names.
- Add equality as a primitive binary connective.
- There's currently working implementations of propositional and modal logic in
future.js, however they need to be refactored.