ILogic

logic.spad line 2454 [edit on github]

ILogic is an algebra with true, false and other 'unproven' values

/\ : (%, %) -> %

from MeetSemilattice

= : (%, %) -> Boolean

returns true (boolean true) if Intuitionistic Logic values are the same. Translates from Intuitionistic Logic to Boolean Logic

T : () -> %

from BoundedMeetSemilattice

\/ : (%, %) -> %

from JoinSemilattice

_|_ : () -> %

from BoundedJoinSemilattice

atom? : % -> Boolean

returns true if this is an atom, that is a leaf node otherwise return false if this is a compound term

coerce : % -> OutputForm

from CoercibleTo(OutputForm)

deductions : List(%) -> List(%)

assumes ln contains a list of factors which must be true for the whole to be true (such as the list produced by factor). From this deductions attempts to produce a list of other proposition that must also be true by using modus ponens. This is used to determine the returned type when converting ILogic to types by using the Curry-Howard isomorphism.

factor : % -> List(%)

splits n into a list of factors which must be true for the whole to be true. This assumes that the top level is already a set of factors separated by /\ otherwise the result will just be a list with one entry: 'n'. This is used when converting ILogic to types by using the Curry-Howard isomorphism.

getChildren : % -> List(%)

returns child nodes if this is a compound term otherwise returns []

implies : (%, %) -> %

implies(a, b) returns the logical implication of ILogic a and b. a is premise, b is conclusion, result is false (contradiction) if premise=true and conclusion=false does not mean there is a causal connection

latex : % -> String

from SetCategory

logicF : () -> %

false (contradiction) is a logical constant.

logicT : () -> %

true is a logical constant.

opType : % -> Symbol

if this is a compound op then opType returns the type of that op: "IMPLY"::Symbol =implies "AND"::Symbol=/\ "OR"::Symbol=\/ "NOT"::Symbol=~ "OTHER"::Symbol=not compound op

parseIL : String -> %

Constructs intuitionistic logic terms from a string notation assumes format like this: <term> : := var | <term>/\spad<term> | <term>\/<term> | <term>-><term> | "("<term>")"

parseIL2 : (String, NonNegativeInteger) -> Record(rft : %, pout : NonNegativeInteger)

Constructs intuitionistic logic terms from a string notation assumes format like this: <term2> : := var | "("<term>")" <term> : := var | <term>/\spad<term> | <term>\/<term> | <term>-><term> | "("<term>")"

parseILTerm : (String, NonNegativeInteger) -> Record(rft : %, pout : NonNegativeInteger)

parseTerm is used by parseIL. It would rarely be called externally but it is here to allow it to call parseIL that is to allow circular calls

proposition : String -> %

Constructs a proposition

redux : % -> %

attempt to simplify theory apply recursively to subnodes normally this should not be necessary since logic values are interpreted when constructed

toString : % -> String

creates a string representation of this term and its sub-terms

toStringUnwrapped : % -> String

similar to 'toString' but does not put outer compound terms in brackets

value : % -> Symbol

returns: "T"::Symbol = T "F"::Symbol = _|_ "E"::Symbol = error "P"::Symbol = proposition "C"::Symbol = compound Constructs lambda term and bind any variables with the name provided

~ : % -> %

~(x) returns the logical complement of x. TODO not sure if complement should be included here? intuitionistic logic can have complement but has different axioms to complement in Boolean algebra. Equivalent capability can be provided by implication.

~= : (%, %) -> Boolean

from BasicType

BoundedLattice

BoundedJoinSemilattice

CoercibleTo(OutputForm)

BoundedMeetSemilattice

SetCategory

MeetSemilattice

BasicType

JoinSemilattice