c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig TruthPF = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePF %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Truth %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder trueI : ded true.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig FalsityPF = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePF %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Falsity %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder falseE : ded false -> {A} ded A.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig NEGPF = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePF %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include NEG %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder notI : (ded A -> {B} ded B) -> ded (not A).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder notE : ded not A -> ded A -> {B} ded B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig IMPPF = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePF %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include IMP %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder impI : (ded A -> ded B) -> ded (A imp B).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder impE : ded (A imp B) -> ded A -> ded B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig CONJPF = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePF %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include CONJ %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder andI : ded A -> ded B -> ded (A and B).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder andEl : ded (A and B) -> ded A.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder andEr : ded (A and B) -> ded B.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig DISJPF = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePF %open ded.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include DISJ %open or.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orIl : ded A -> ded (A or B).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orIr : ded B -> ded (A or B).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orE : ded (A or B) -> (ded A -> ded C) -> (ded B -> ded C) -> ded C.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePF %open ded.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include NEG %open not.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include DISJ %open or.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder tnd : ded (A or (not A)).