// Written by Terence Tao. This work is licensed under a Creative Commons Attribution 4.0 International License: http://creativecommons.org/licenses/by/4.0/
/// Global variables
sentences = []; // sentences[name] is a sentence/term attached to a name string; easier to populate this dynamically than to create a general string to sentence/term parser.
unlockedLaws = [];
numLaws = 0; // used to give each law a numerical index with which to detect circularity
// convert a list of sentences, boxes, or contexts to a string
function listToString(list) {
if (list.length == 0) return "";
var i;
var str = "";
for (i = 0; i < list.length; i++) {
str += toContext(list[i]).name + ", ";
}
str = str.substring(0, str.length - 2);
return str;
}
// create a deduction string
function deductionString(prefix, list, conclusion)
{
if (list.length == 0) {
if (conclusion.type == "environment")
return "Form environment " + conclusion.name + ".";
else
return "Deduce " + conclusion.name + ".";
}
else {
if (conclusion.type == "environment")
return prefix + " " + listToString(list) + ": form environment " + conclusion.name + ".";
else
return prefix + " " + listToString(list) + ": deduce " + conclusion.name + ".";
}
}
//// FreeVariable object
function FreeVariable(name)
{
this.type = "free variable";
this.subtype = name;
this.name = ""+name+"";
this.longName = this.name;
}
// the name of a free variable associated to a non-negative integer i. Note: this is the name without the italics; should be matched to the "subtype" of a variable rather than its name.
function FreeVariableName(i) {
var str;
switch(i % 3) {
case 0: str = 'x'; break;
case 1: str = 'y'; break;
case 2: str = 'z'; break;
}
var j;
for (j=0; j < (i-2)/3; j++) str += "'";
return str;
}
//// BoundVariable object. In this text, it is assumed that free and bound variables have disjoint namespaces; we'll use x,y,z,x',y', etc. for free variables and X,Y,Z,X',Y',etc. for bound variables. Note: this is the name without the italics; should be matched to the "subtype" of a variable rather than its name.
function BoundVariable(name)
{
this.type = "bound variable";
this.subtype = name;
this.name = ""+name+"";
this.longName = this.name;
}
/// the name of a bound variable associated to a non-negative integer i
function BoundVariableName(i) {
var i;
switch(i % 3) {
case 0: str = 'X'; break;
case 1: str = 'Y'; break;
case 2: str = 'Z'; break;
}
var j;
for (j=0; j < (i-2)/3; j++) str += "'";
return str;
}
/// Operator object. relationStyle is for 2-ary operators placed in between the arguments, e.g. x+y, as opposed to f(x,y).
function Operator( name, arity, relationStyle )
{
this.type = "operator";
this.subtype = name;
this.name = "" + name + "";
this.arity = arity;
this.relationStyle = relationStyle;
switch(this.arity)
{
case 0: this.longName = "Constant " + this.name; break;
case 1: this.longName = "Unary operator " + this.name + "()"; break;
case 2:
if (this.relationStyle) this.longName = "Binary operator " + this.name;
else this.longName = "Binary operator " + this.name + "(,)";
}
}
/// Term object. The only way to make a term is to use a free or bound variable or primitive term, or to apply an operator with a list of terms.
function Term()
{
this.type = "term";
this.subtype = ""; // will be "free variable", "bound variable", "primitive", or "operator evaluation"
this.name = "";
this.longName = "";
this.operator = ""; // the operator used (only needed for operator subtype)
this.argList = []; // list of args, or just the variable
}
// turn a free variable into a term
function freeVariableTerm(free)
{
var term = new Term();
term.subtype = "free variable";
term.name = free.name;
term.longName = free.longName;
term.argList = [free];
return term;
}
// turn a bound variable into a term
function boundVariableTerm(bound)
{
var term = new Term();
term.subtype = "bound variable";
term.name = bound.name;
term.longName = bound.longName;
term.argList = [bound];
return term;
}
// turn an operator and some arguments into a term
function operatorTerm(operator, argList)
{
var term = new Term();
term.subtype = "operator evaluation";
var i;
term.operator = operator;
for (i=0; i < term.operator.arity; i++)
term.argList[i] = toTerm(argList[i]);
if (term.operator.relationStyle) {
term.name = term.argList[0].longName + " " + term.operator.name + " " + term.argList[1].longName;
term.longName = "(" + term.name + ")";
} else if (term.operator.arity == 0) {
term.name = term.operator.name;
term.longName = term.name;
} else {
var str = term.operator.name + "(";
for (i = 0; i < term.operator.arity; i++ )
str += term.argList[i].name + ", ";
str = str.substring(0, str.length - 2);
term.name = str + ")";
term.longName = term.name;
}
return term;
}
function primitiveTerm(name)
{
var term = new Term();
term.subtype = "primitive";
term.name = name;
term.longName = name;
return term;
}
// turn an object into a term if possible
function toTerm(obj)
{
if (typeof(obj) == "string") return primitiveTerm(obj);
if (obj.type == "term") return obj;
if (obj.type == "free variable") return freeVariableTerm(obj);
if (obj.type == "bound variable") return boundVariableTerm(obj);
error("Unrecognised type for conversion to term.");
}
/// Predicate object. relationStyle is for 2-ary predicates placed in between the arguments, e.g. x=y, as opposed to P(x,y).
function Predicate( name, arity, relationStyle )
{
this.type = "predicate";
this.subtype = name;
this.name = "" + name + "";
this.arity = arity;
this.relationStyle = relationStyle;
switch(this.arity)
{
case 0: this.longName = "Proposition " + this.name; break;
case 1: this.longName = "Predicate " + this.name + "()"; break;
case 2:
if (this.relationStyle) this.longName = "Relation " + this.name;
else this.longName = "Predicate " + this.name + "(,)";
}
}
// we have one special predicate: the equality relation
var equality = new Predicate("=", 2, true);
// the sentence x=y
function equals(x,y) {
return predicateSentence( equality, [x,y] );
}
//// Connective object
function Connective(name, arity) {
this.name = name; // "AND", "OR", "NOT", "IMPLIES", "IFF", "TRUE", "FALSE"
this.arity = arity; // 0, 1, or 2
}
var ANDConnective = new Connective("AND", 2);
var ORConnective = new Connective("OR", 2);
var NOTConnective = new Connective("NOT", 1);
var IMPLIESConnective = new Connective("IMPLIES", 2);
var IFFConnective = new Connective("IFF", 2);
var TRUEConnective = new Connective("TRUE", 0);
var FALSEConnective = new Connective("FALSE", 0);
//// Sentence object
function Sentence() {
this.type = ""; // "primitive", "connective", "quantifier"
this.subtype = ""; // "AND", "OR", "NOT", "IMPLIES", "IFF" for connectives; "atomic" or "predicate" for primitives; "for all" or "there exists" for quantifiers
this.name = ""; // name of sentence when used standalone
this.longName = ""; // name of sentence when combined with other sentences
this.argList = []; // the list of arguments in this sentence (usually of length 0, 1, or 2)
this.predicate = ""; // the predicate used (only relevant for predicate subtype)
this.connective = ""; // the connective used (only relevant for connective subtype)
}
// create an atomic sentence
function atomicSentence(name) {
var sentence = new Sentence();
sentence.type = "primitive";
sentence.subtype = "atomic";
sentence.name = ""+name+"";
sentence.longName = sentence.name;
return sentence;
}
// create a sentence from predicate and args
function predicateSentence(predicate, argList) {
var sentence = new Sentence;
sentence.type = "primitive";
sentence.subtype = "predicate";
sentence.predicate = predicate;
var i;
for (i=0; i < argList.length; i++)
sentence.argList[i] = toTerm(argList[i]);
if (sentence.predicate.relationStyle) {
sentence.name = argList[0].longName + " " + sentence.predicate.name + " " + argList[1].longName;
sentence.longName = "(" + sentence.name + ")";
} else if (sentence.predicate.arity == 0) {
sentence.name = sentence.predicate.name;
sentence.longName = sentence.name;
} else {
var str = sentence.predicate.name + "(";
for (i = 0; i < sentence.predicate.arity; i++ )
str += toTerm(argList[i]).name + ", ";
str = str.substring(0, str.length - 2);
sentence.name = str + ")";
sentence.longName = sentence.name;
}
sentence.name = sentence.name;
return sentence;
}
// from a sentence from a connective and list of arguments
function connectiveSentence(connective, argList) {
var sentence = new Sentence();
sentence.type = "connective";
sentence.subtype = connective.name;
sentence.argList = argList;
sentence.connective = connective;
switch(connective.arity) {
case 0:
sentence.name = connective.name;
sentence.longName = sentence.name;
break;
case 1:
sentence.name = connective.name + " " + argList[0].longName;
sentence.longName = "(" + sentence.name + ")";
break;
case 2:
sentence.name = argList[0].longName + " " + connective.name + " " + argList[1].longName;
sentence.longName = "(" + sentence.name + ")";
break;
}
return sentence;
}
// form the conjunction of two sentences
function AND( sentence1, sentence2) {
return connectiveSentence(ANDConnective, [sentence1, sentence2]);
}
// form the disjunction of two sentences
function OR( sentence1, sentence2) {
return connectiveSentence(ORConnective, [sentence1, sentence2]);
}
// form the implication of two sentences
function IMPLIES( sentence1, sentence2) {
return connectiveSentence(IMPLIESConnective, [sentence1, sentence2]);
}
// form the iff of two sentences
function IFF( sentence1, sentence2) {
return connectiveSentence(IFFConnective, [sentence1, sentence2]);
}
// form the negation of a sentence
function NOT( sentence1) {
return connectiveSentence(NOTConnective, [sentence1]);
}
// form the TRUE sentence
function TRUE() {
return connectiveSentence(TRUEConnective, []);
}
// form the FALSE sentence
function FALSE() {
return connectiveSentence(FALSEConnective, []);
}
// a sentence of the form "for all : "
function forAll(predicate, bound) {
var sentence = new Sentence();
sentence.type = "quantifier";
sentence.subtype = "for all";
sentence.name = "FOR ALL " + bound.name + ": " + predicate.longName;
sentence.longName = "(" + sentence.name + ")";
sentence.argList = [predicate, bound];
sentence.name = sentence.name;
return sentence;
}
// a sentence of the form "there exists : "
function thereExists(predicate, bound) {
var sentence = new Sentence();
sentence.type = "quantifier";
sentence.subtype = "there exists";
sentence.name = "THERE EXISTS " + bound.name + ": " + predicate.longName;
sentence.longName = "(" + sentence.name + ")";
sentence.argList = [predicate, bound];
sentence.name = sentence.name;
return sentence;
}
// tries to convert an obj to sentence if it can
function toSentence(obj) {
if (typeof(obj) == 'string') return atomicSentence(obj);
if (obj instanceof Sentence ) return obj;
if (obj instanceof Context ) return obj.sentence;
if (obj instanceof Law) return obj.conclusion.sentence;
if (obj instanceof Exercise) return obj.law.conclusion.sentence;
if (obj instanceof Assumption) return obj.sentence;
if (obj.type == "sentenceBox") return obj.sentence;
if (obj.type == "formulaBox") return obj.sentence;
error("Unable to convert object to sentence.");
}
// Law object
function Law(name, givens, conclusion) {
numLaws++;
this.name = name; // name of law, e.g. "EXERCISE 1"
// givens is an array of given hypotheses (can be empty). I allow sentences as givens, so these need to be converted to contexts.
var givenslist = [];
givens.forEach( function(given) {
givenslist.push(toContext(given));
});
this.givens = givenslist;
this.conclusion = toContext(conclusion); // given conclusion
this.unlocked = false; // by default the law is not unlocked
this.string = deductionString("Given", givens, this.conclusion);
this.desc = ""+name+": " + this.string;
this.index = numLaws; // the order in which the law was unlocked (used to determine circularity)
this.clone = ""; // points to the clone of the law with additional root environment, if needed
if (localStorage)
if (localStorage.getItem("law " + this.name) != null)
unlock(this, localStorage.getItem("law " + this.name));
if (allFormulas(this.givens)) {
if (this.conclusion.type == 'sentence in environment' || this.conclusion.type == 'environment') {
var givensClone = this.givens.slice(0);
givensClone.push(rootEnvironmentContext());
this.clone = new Law(this.name, givensClone, this.conclusion);
}
}
}
// add (name of) expr to list if not already there
function record(list, expr) {
if (!list.includes(expr.name)) {
list.push(expr.name);
sentences[expr.name] = expr; // remember the variable object associated to name
}
}
// list the (names of) atomic primitives, free variables, bound variables, primitive terms, predicates, operators occurring in a law
function listPrimitives(law, getPrimitives, getFreeVars, getBoundVars, getPrimTerms, getPredicates, getOperators, getAtomic) {
var list = [];
law.givens.forEach( function(item) {
pushPrimitivesFromContext(list, toContext(item), getPrimitives, getFreeVars, getBoundVars, getPrimTerms, getPredicates, getOperators, getAtomic);
});
// usually the line below is redundant, as any primitives in conclusion should have already appeared in one of the givens, but there are some exceptions, e.g. universal introduction without specifying the bound variable
pushPrimitivesFromContext(list, law.conclusion, getPrimitives, getFreeVars, getBoundVars, getPrimTerms, getPredicates, getOperators, getAtomic);
return list;
}
// push all the primitives from context onto list (removing duplicates)
function pushPrimitivesFromContext(list, context, getPrimitives, getFreeVars, getBoundVars, getPrimTerms, getPredicates, getOperators, getAtomic) {
if (context.type == "formula" || context.type == "sentence in environment") {
pushPrimitivesFromSentence(list, context.sentence, getPrimitives, getFreeVars, getBoundVars, getPrimTerms, getPredicates, getOperators, getAtomic);
}
if (context.type == "environment" || context.type == "sentence in environment")
{
context.environment.forEach( function(item) {
if (item.type == "assuming" || item.type == "setting") {
pushPrimitivesFromSentence(list, item.sentence, getPrimitives, getFreeVars, getBoundVars,getPrimTerms, getPredicates, getOperators, getAtomic);
}
if (item.type == "setting" || item.type == "letting") {
if (getFreeVars) {
record(list, item.variable);
}
}
});
}
if (context.type == "term context") {
pushPrimitivesFromSentence(list, context.term, getPrimitives, getFreeVars, getBoundVars,getPrimTerms,getPredicates, getOperators, getAtomic);
}
}
// push all the primitives from sentence/term onto list (removing duplicates)
function pushPrimitivesFromSentence(list, sentence, getPrimitives, getFreeVars, getBoundVars,getPrimTerms,getPredicates, getOperators, getAtomic)
{
switch(sentence.type) {
case "primitive":
if (getPrimitives) record(list, sentence);
switch(sentence.subtype) {
case "atomic":
if (getAtomic) record(list, sentence);
break;
case "predicate":
if (getPredicates) record(list, sentence.predicate);
sentence.argList.forEach( function(arg) { pushPrimitivesFromSentence(list,arg, getPrimitives, getFreeVars, getBoundVars,getPrimTerms,getPredicates, getOperators, getAtomic);} );
break;
}
break;
case "quantifier":
if (getBoundVars) record(list, sentence.argList[1]);
pushPrimitivesFromSentence(list, sentence.argList[0], getPrimitives, getFreeVars, getBoundVars,getPrimTerms,getPredicates, getOperators, getAtomic);
break;
case "connective":
sentence.argList.forEach( function(arg) { pushPrimitivesFromSentence(list,arg, getPrimitives, getFreeVars, getBoundVars,getPrimTerms,getPredicates, getOperators, getAtomic);} );
break;
case "term":
switch(sentence.subtype) {
case "primitive":
if (getPrimTerms) record(list,sentence);
return;
case "operator evaluation":
if (getOperators) record(list, sentence.operator);
sentence.argList.forEach( function(arg) { pushPrimitivesFromSentence(list,arg, getPrimitives, getFreeVars, getPrimTerms,getPredicates, getOperators, getAtomic);} );
return;
case "free variable":
if (getFreeVars) record(list, sentence.argList[0]);
return;
case "bound variable":
if (getBoundVars) record(list, sentence.argList[0]);
return;
}
}
}
// returns true if all terms in givens are formulas or terms (i.e., no environment is involved)
function allFormulas(givens) {
var i;
for (i = 0; i < givens.length; i++) {
if (givens[i].type != "formula" && givens[i].type != "term context") return false;
}
return true;
}
// a tricky routine: tries to match arglist to the givens of a law and see what the primitives are, returning this data in an output object. Note: for predicate logic, some of the matches need to be discarded because the conclusion does not obey scoping laws (e.g. repeated free variables, etc.). Also there may be situations where there are multiple possible substitutions (creating existential quantifier)
function matchWithGivens( arglist, law, primitives ) {
var givens = law.givens;
var conclusion = law.conclusion;
var output = new Object();
output.matches = true; // so far, no reason to doubt a match.
output.illegal = false; // sometimes there is technically a match but something is ill-formed
output.multivalued = false; // do we need multiple conclusions, or just one?
output.env = []; // by default, the output environment will be the root one.
primitives.forEach( function(primitive) {
output[primitive] = "";
});
// technically one needs to ensure that primitives and free variables avoid reserved words such as "matches". This is unlikely to come up in practice.
if (arglist.length != givens.length) {
output.matches = false;
return output;
}
// convert everything to contexts if not already done so (this step may be redundant)
var i;
for (i = 0; i < givens.length; i++) {
arglist[i] = toContext(arglist[i]);
givens[i] = toContext(givens[i]);
}
// check if all the givens are formulas
if (!allFormulas(givens))
{
var proposedYet = false;
var proposedEnv = [];
for (i = 0; i < givens.length; i++) {
if (givens[i].type == "sentence in environment" || givens[i].type == "environment") {
if (arglist[i].environment.length < givens[i].environment.length) {
// can't match if the template has more deeply nested assumptions than the arglist!
output.matches = false;
return output;
}
var candidateEnv = arglist[i].environment.slice( 0, arglist[i].environment.length - givens[i].environment.length);
if (proposedYet == false) {
proposedYet = true;
proposedEnv = candidateEnv;
}
else if (assumptionListToString(proposedEnv) != assumptionListToString(candidateEnv)) { // need to convert to string here as a proxy for passing by value rather than by reference
output.matches = false;
return output;
}
}
}
output.env = proposedEnv;
}
switch(law) { // a number of laws are too complex to be matched by the standard algorithm and have to be treated separately
case universalIntroduction:
case universalIntroduction2:
matchUniversalIntroduction(arglist, output, law);
break;
case universalSpecification:
case universalSpecification2:
matchUniversalSpecification(arglist, output, law);
break;
case existentialInstantiation:
case existentialInstantiation2:
matchExistentialInstantiation(arglist, output, law);
break;
case existentialIntroduction:
case existentialIntroduction2:
matchExistentialIntroduction(arglist, output, law);
break;
case indiscernability:
matchIndiscernability(arglist, output, law);
break;
default:
var i;
for (i = 0; i < givens.length; i++) {
matchWithGiven( arglist[i], givens[i], output);
if (!output.matches) return output;
}
for (i=0; i < primitives.length; i++) {
if (output[primitives[i]] == "") { // somehow failed to match one of the primitives
output.matches = false;
return output;
}
}
output.conclusion = subs(conclusion, output);
}
return output;
}
// match arglist against one of the two laws of universal introduction and report the conclusions in output
function matchUniversalIntroduction(arglist, output, law) {
if (!output.matches) return;
// arglist[0] needs to be of the form "A, [letting x be arbitrary]" after the output.env
if (arglist[0].type != "sentence in environment") {
output.matches = false;
return;
}
var assumption = arglist[0].environment[output.env.length];
if (assumption.type != "letting") {
output.matches = false;
return;
}
var freeVariable = assumption.variable;
var statement = arglist[0].sentence;
var boundVariable;
switch (law) {
case universalIntroduction:
if (arglist[1].type != "term context") {
output.matches = false;
return;
}
if (arglist[1].term.subtype != "bound variable") {
output.matches = false;
return;
}
boundVariable = arglist[1].term.argList[0];
break;
case universalIntroduction2:
if (arglist[1].type != "environment") {
output.matches = false;
return;
}
// choose the next available bound Variable
boundVariable = nextAvailableBoundVariable(statement);
break;
}
var newSentence = forAll( searchReplace( statement, freeVariable, boundVariable), boundVariable);
output.conclusion = sentenceContext( newSentence, output.env );
}
// return the next availalbe bound variable not already in a statement
function nextAvailableBoundVariable(statement) {
var boundVars = [];
pushPrimitivesFromSentence(boundVars, statement, false, false, true,false, false, false, false);
var num=0;
var match;
var str, longStr;
do {
str = BoundVariableName(num);
longStr = ""+str+"";
match = boundVars.includes(longStr);
num++;
} while (match);
return new BoundVariable(str);
}
// match arglist against the law of universal specification and report the conclusions in output
function matchUniversalSpecification(arglist, output, law) {
if (!output.matches) return;
// arglist[0] needs to be of the form "FOR ALL X: P(X)" after the output.env
if (arglist[0].type != "sentence in environment") {
output.matches = false;
return;
}
if (arglist[0].sentence.type != "quantifier" || arglist[0].sentence.subtype != "for all") {
output.matches = false;
return;
}
var sentence = arglist[0].sentence.argList[0];
var boundVar = toTerm(arglist[0].sentence.argList[1]).argList[0];
if (arglist[1].type != "term context") {
output.matches = false;
return;
}
var term = toTerm(arglist[1].term);
var newSentence = searchReplace( sentence, boundVar, term );
if (law == universalSpecification) {
if (hasBoundOrUnknownFree(term, output.env)) {
output.illegal = true; // will keep matching but will display in silver
}
output.conclusion = sentenceContext( newSentence, output.env );
} else if (law == universalSpecification2) {
if (term.subtype != "free variable") {
output.matches = false;
return;
}
var env = output.env.slice(0);
env.push(toAssumption(term.argList[0]));
output.conclusion = sentenceContext( newSentence, env );
}
}
// returns true if term contains a bound variable
function hasBoundOrUnknownFree(term,env) {
switch(term.subtype) {
case "primitive":
return false;
case "free variable":
var i;
for (i=0; i < env.length; i++)
if (env[i].type == 'letting' || env[i].type == 'setting')
if (env[i].variable.name == term.argList[0].name)
return false;
return true;
case "bound variable":
return true;
case "operator":
var i;
for (i=0; i < term.argList.length; i++)
if (hasBoundOrUnknownFree(term.argList[i],env)) return true;
return false;
}
}
// replace all occurrences of term "search" with term "replace"
function searchReplace(statement, search, replace) {
var newArgList = [];
var i;
if (statement.type == "free variable" || statement.type == "bound variable") return statement;
if (statement.name == search.name) return toTerm(replace);
for (i=0; i < statement.argList.length; i++)
newArgList[i] = searchReplace(statement.argList[i], search, replace);
switch (statement.type) {
case "term":
if (statement.subtype == "free variable") return statement;
if (statement.subtype == "bound variable") return statement;
if (statement.subtype == "primitive") return statement;
if (statement.subtype == "operator evaluation") return operatorTerm(statement.operator, newArgList);
return;
case "primitive":
if (statement.subtype == "atomic") return statement;
if (statement.subtype == "predicate") return predicateSentence(statement.predicate, newArgList);
return;
case "connective":
return connectiveSentence(statement.connective, newArgList);
case "quantifier":
if (statement.subtype == "for all") return forAll( newArgList[0], newArgList[1]);
if (statement.subtype == "there exists") return thereExists( newArgList[0], newArgList[1]);
return;
}
}
// match arglist against the law of existential instantiation and report the conclusions in output
function matchExistentialInstantiation(arglist, output, law) {
if (!output.matches) return;
// arglist[0] needs to be of the form "THERE EXISTS X: P(X)" after the output.env
if (arglist[0].type != "sentence in environment") {
output.matches = false;
return;
}
if (arglist[0].sentence.type != "quantifier" || arglist[0].sentence.subtype != "there exists") {
output.matches = false;
return;
}
var sentence = arglist[0].sentence.argList[0];
var boundVar = toTerm(arglist[0].sentence.argList[1]).argList[0];
var freeVariable;
if (law == existentialInstantiation) {
if (arglist[1].type != "term context") {
output.matches = false;
return;
}
if (arglist[1].term.subtype != "free variable") {
output.matches = false;
return;
}
freeVariable = arglist[1].term.argList[0];
} else if (law == existentialInstantiation2) {
// choose the next available free Variable
var freeVars = [];
pushPrimitivesFromContext(freeVars, sentenceContext(sentence,output.env), false, true, false, false, false, false, false);
var num=0;
var match;
var str, longStr;
do {
str = FreeVariableName(num);
longStr = ""+str+"";
match = freeVars.includes(longStr);
num++;
} while (match);
freeVariable = new FreeVariable(str);
}
var newSentence = searchReplace( sentence, boundVar, freeVariable );
var env = output.env.slice(0);
env.push( settingAssumption(newSentence, freeVariable) );
output.conclusion = sentenceContext( newSentence, env );
}
// match arglist against one of the two laws of existential introduction and report the conclusions in output
function matchExistentialIntroduction(arglist, output, law) {
if (!output.matches) return;
// arglist[0] needs to be of the form "P(X)" after the output.env
if (arglist[0].type != "sentence in environment") {
output.matches = false;
return;
}
var sentence = arglist[0].sentence;
// arglist[1] needs to be a term context
if (arglist[1].type != "term context") {
output.matches = false;
return;
}
var term = arglist[1].term;
if (hasBoundOrUnknownFree(term, output.env)) {
output.illegal = true; // will keep matching but will display in silver
}
var boundVariable;
switch (law) {
case existentialIntroduction2:
if (arglist[2].type != "term context") {
output.matches = false;
return;
}
if (arglist[2].term.subtype != "bound variable") {
output.matches = false;
return;
}
boundVariable = arglist[2].term.argList[0];
break;
case existentialIntroduction:
// choose the next available bound Variable
boundVariable = nextAvailableBoundVariable(sentence);
break;
}
output.multivalued = true;
var translations = allSearchReplace(sentence, term, boundVariable);
output.conclusions = [];
var i;
for (i=0; i < translations.length; i++)
output.conclusions.push(sentenceContext( thereExists(translations[i],boundVariable), output.env ));
}
// match arglist against the law of indiscernability and report the conclusions in output
function matchIndiscernability(arglist, output, law) {
if (!output.matches) return;
// arglist[0], arglist[1] have to be sentences
if (arglist[0].type != "sentence in environment" || arglist[1].type != "sentence in environment") {
output.matches = false;
return;
}
var sentence = arglist[0].sentence;
var sentence2 = arglist[1].sentence;
// sentence2 needs to be of the form alpha=beta
if (sentence2.subtype != "predicate" || sentence2.predicate != equality) {
output.matches = false;
return;
}
var alpha = sentence2.argList[0];
var beta = sentence2.argList[1];
output.multivalued = true;
var translations = allSearchReplace(sentence, alpha, beta);
output.conclusions = [];
var i;
for (i=0; i < translations.length; i++)
if (translations[i].name != sentence.name) //remove trivial applications of indiscernability in which ibe deduces a sentence from itself
output.conclusions.push(sentenceContext( translations[i], output.env ));
}
// return a list of all possible ways in which appearances of "search" in sentence can be replaced with "replace"
function allSearchReplace(statement, search, replace)
{
if (statement.type == "free variable" || statement.type == "bound variable") return [statement];
var list = [];
var newArgList = [];
var i,j;
if (statement.name == search.name) list.push(toTerm(replace));
for (i=0; i < statement.argList.length; i++)
newArgList[i] = allSearchReplace(statement.argList[i], search, replace);
switch (statement.type) {
case "term":
switch (statement.subtype) {
case "free variable":
case "bound variable":
case "primitive":
list.push(statement);
break;
case "operator evaluation":
switch(statement.operator.arity) {
case 0:
list = [operatorTerm(statement.operator, [])];
break;
case 1:
for (i=0; i < newArgList[0].length; i++)
list.push( operatorTerm(statement.operator, [newArgList[0][i]]));
break;
case 2:
for (i=0; i < newArgList[0].length; i++)
for (j=0; j < newArgList[1].length; j++)
list.push( operatorTerm( statement.operator, [newArgList[0][i], newArgList[1][j]]));
break;
}
break;
}
break;
case "primitive":
switch(statement.subtype) {
case "atomic":
list.push(statement);
break;
case "predicate":
switch(statement.predicate.arity) {
case 0:
list.push(predicateSentence(statement.predicate, []));
break;
case 1:
for (i=0; i < newArgList[0].length; i++)
list.push( predicateSentence(statement.predicate, [newArgList[0][i]]));
break;
case 2:
for (i=0; i < newArgList[0].length; i++)
for (j=0; j < newArgList[1].length; j++)
list.push( predicateSentence( statement.predicate, [newArgList[0][i], newArgList[1][j]]));
break;
}
break;
}
break;
case "connective":
switch(statement.connective.arity) {
case 0:
list.push(connectiveSentence(statement.connective, []));
break;
case 1:
for (i=0; i < newArgList[0].length; i++)
list.push( connectiveSentence(statement.connective, [newArgList[0][i]]));
break;
case 2:
for (i=0; i < newArgList[0].length; i++)
for (j=0; j < newArgList[1].length; j++)
list.push( connectiveSentence( statement.connective, [newArgList[0][i], newArgList[1][j]]));
break;
}
break;
case "quantifier":
switch(statement.subtype) {
case "for all":
for (i=0; i < newArgList[0].length; i++)
for (j=0; j < newArgList[1].length; j++)
list.push( forAll( newArgList[0][i], newArgList[1][j]));
break;
case "there exists":
for (i=0; i < newArgList[0].length; i++)
for (j=0; j < newArgList[1].length; j++)
list.push( thereExists( newArgList[0][i], newArgList[1][j]));
break;
}
break;
}
return list;
}
// try to match a context with a template context and store the match in output
function matchWithGiven( context, template, output) {
if (!output.matches) return;
if (context.type != template.type) {
output.matches = false;
return;
}
if (template.type == "environment" || template.type == "sentence in environment") {
var i;
for (i = 0; i < template.environment.length; i++) {
matchWithGivenAssumption( context.environment[i + output.env.length], template.environment[i], output);
if (!output.matches) return;
}
}
if (template.type == "formula" || template.type == "sentence in environment")
matchWithGivenSentence( context.sentence, template.sentence, output);
if (template.type == "term context")
matchWithGivenSentence( context.term, template.term, output);
}
// match item to template object in output if this has not already been done
function makeMatch(item, template, output) {
if (item.name == output[template.name].name) {
// good, it matches what we've already fit to the template!
return;
}
if (output[template.name] == "") {
output[template.name] = item;
return;
}
output.matches = false;
return;
}
// try to match an assumption with a template sentence and store the match in output
function matchWithGivenAssumption( assumption, template, output) {
if (!output.matches) return;
if (assumption.type != template.type) {
output.matches = false;
return;
}
if (assumption.type == 'assuming' || assumption.type == 'setting') {
matchWithGivenSentence( assumption.sentence, template.sentence, output);
}
if (assumption.type == 'letting' || assumption.type == 'setting') {
makeMatch(assumption.variable, template.variable, output);
}
}
// try to match a sentence or term with a template and store the match in output
function matchWithGivenSentence( sentence, template, output) {
if (!output.matches) return;
switch (template.type) {
case "primitive":
switch (template.subtype) {
case "atomic":
makeMatch(sentence,template,output);
return;
case "predicate":
if (template.predicate == equality) {
if (sentence.predicate != equality) {
output.matches = false;
return;
}
var i;
for (i=0; i