kdrag.theories.logic.intuitionistic

Module Attributes

Prop	A proposition is a world valuation function.
or_intro2	Finite model property +

Functions

And(*ps)	w |= (A /B)[e] if and only if w |= A[e] and w |= B[e]
Const(name, sort)
Implies(p, q)
Not(p)
Or(*ps)	w |= (A / B)[e] if and only if w |= A[e] or w |= B[e]
Sort(sort)
Valid(p)

kdrag.theories.logic.intuitionistic.And(*ps: DatatypeRef) → DatatypeRef

w |= (A /B)[e] if and only if w |= A[e] and w |= B[e]

>>> p, q = smt.Consts("p q", Prop)
>>> And(p,q)
Prop(Lambda(w, And(val(p)[w], val(q)[w])))

Parameters:

ps (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.logic.intuitionistic.Const(name: str, sort: SortRef) → DatatypeRef

Parameters:

• name (str)

• sort (SortRef)

Return type:

DatatypeRef

kdrag.theories.logic.intuitionistic.Implies(p: DatatypeRef, q: DatatypeRef) → DatatypeRef

Parameters:

• p (DatatypeRef)

• q (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.logic.intuitionistic.Not(p: DatatypeRef) → DatatypeRef

Parameters:

p (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.logic.intuitionistic.Or(*ps: DatatypeRef) → DatatypeRef

w |= (A / B)[e] if and only if w |= A[e] or w |= B[e]

>>> p, q = smt.Consts("p q", Prop)
>>> Or(p,q)
Prop(Lambda(w, Or(val(p)[w], val(q)[w])))

Parameters:

ps (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.logic.intuitionistic.Prop = Prop

A proposition is a world valuation function. Propositions become monotonically more true as we move to more accessible worlds. Note that Prop ~ Sort(Unit)

Parameters:

args (ExprRef)

Return type:

DatatypeRef

kdrag.theories.logic.intuitionistic.Sort(sort: SortRef)

Parameters:

sort (SortRef)

kdrag.theories.logic.intuitionistic.Valid(p: DatatypeRef) → BoolRef

Parameters:

p (DatatypeRef)

Return type:

BoolRef

kdrag.theories.logic.intuitionistic.or_intro2 = |= ForAll([a, b],        Implies(And(ForAll([w, u],                           Implies(And(acc(w, u), val(a)[w]),                                   val(a)[u])),                    ForAll([w, u],                           Implies(And(acc(w, u), val(b)[w]),                                   val(b)[u]))),                ForAll(w,                       val(Prop(Lambda(w,                                       ForAll(u,                                         Implies(acc(w, u),                                         Implies(val(b)[u],                                         val(Prop(Lambda(w,                                         Or(val(a)[w],                                         val(b)[w]))))[u]))))))[w])))

Finite model property +

Parameters:

args (smt.ExprRef | Proof)