lset.mm

$( set.mm - Version of 17-May-2019 $)
$( Trying to implement https://arxiv.org/abs/1805.07518 and doing a poor job.
There is no original thought here, only data entry. -- CS $)

$(
  This is some linear logic designed to neatly replace classical logic for
  foundational work. I will try to follow set.mm for theorem names and
  structure, and iset.mm for constructive insights.
$)

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
                           Pre-logic
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

  $( Declare the primitive constant symbols for propositional calculus. $)
  $c ( $.  $( Left parenthesis $)
  $c ) $.  $( Right parenthesis $)
  $c wff $. $( Well-formed formula symbol (read:  "the following symbol
               sequence is a wff") $)
  $c |- $. $( Turnstile (read:  "it is true that" or "a proof exists for") $)

  $( wff variable sequence:  ph ps ch th ta et ze si rh mu la ka $)
  $( Introduce some variable names we will use to represent well-formed
     formulas (wff's). $)
  $v ph $.  $( Greek phi $)
  $v ps $.  $( Greek psi $)
  $v ch $.  $( Greek chi $)
  $v th $.  $( Greek theta $)
  $v ta $.  $( Greek tau $)
  $v et $.  $( Greek eta $)
  $v ze $.  $( Greek zeta $)
  $v si $.  $( Greek sigma $)
  $v rh $.  $( Greek rho $)
  $v mu $.  $( Greek mu $)
  $v la $.  $( Greek lambda $)
  $v ka $.  $( Greek kappa $)

  $( Specify some variables that we will use to represent wff's.
     The fact that a variable represents a wff is relevant only to a theorem
     referring to that variable, so we may use $f hypotheses.  The symbol
     ` wff ` specifies that the variable that follows it represents a wff. $)
  $( Let variable ` ph ` be a wff. $)
  wph $f wff ph $.
  $( Let variable ` ps ` be a wff. $)
  wps $f wff ps $.
  $( Let variable ` ch ` be a wff. $)
  wch $f wff ch $.
  $( Let variable ` th ` be a wff. $)
  wth $f wff th $.
  $( Let variable ` ta ` be a wff. $)
  wta $f wff ta $.
  $( Let variable ` et ` be a wff. $)
  wet $f wff et $.
  $( Let variable ` ze ` be a wff. $)
  wze $f wff ze $.
  $( Let variable ` si ` be a wff. $)
  wsi $f wff si $.
  $( Let variable ` rh ` be a wff. $)
  wrh $f wff rh $.
  $( Let variable ` mu ` be a wff. $)
  wmu $f wff mu $.
  $( Let variable ` la ` be a wff. $)
  wla $f wff la $.
  $( Let variable ` ka ` be a wff. $)
  wka $f wff ka $.

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        Recursively define primitive wffs for linear logic
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  $c 0 $. $( Zero $)
  $c 1 $. $( One $)
  $c T $. $( Truth $)
  $c F $. $( Falsity $)

  w0 $a wff 0 $.
  w1 $a wff 1 $.
  wT $a wff T $.
  wF $a wff F $.

  $( The sole unbalanced truth. By choosing a side, we determine the
  orientation of the logic. $)
  ax-1 $a |- 1 $.

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        Linear connectives
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  $( The paramends (turned ampersand) isn't available, sadly. As a result, the
  connectives we're using are the ones from https://arxiv.org/abs/1805.07518 $)
  $c [] $. $( Friend box, multiplicative conjunction (read: "times") $)
  $c <> $. $( Option diamond, multiplicative disjunction (read: "par") $)
  $c |_| $. $( Coproduct, union, additive conjunction (read: "plus") $)
  $c |"| $. $( Product, additive disjunction (read: "with") $)

  wf $a wff ( ph [] ps ) $.
  wo $a wff ( ph <> ps ) $.
  wc $a wff ( ph |_| ps ) $.
  wp $a wff ( ph |"| ps ) $.

  $( [] has unit 1. $)
  ${
    pr-mcuniti $e |- ps $.
    ax-mcuniti $a |- ( ps [] 1 ) $.
  $}
  ${
    pr-mcunite $e |- ( ps [] 1 ) $.
    ax-mcunite $a |- ps $.
  $}

  $( [] commutes. $)
  ${
    pr-mccomm $e |- ( ps [] ph ) $.
    ax-mccomm $a |- ( ph [] ps ) $.
  $}

  $( [] associates. $)
  ${
    pr-mcassl $e |- ( ps [] ( ph [] ch ) ) $.
    ax-mcassl $a |- ( ( ps [] ph ) [] ch ) $.
  $}
  ${
    pr-mcassr $e |- ( ( ps [] ph ) [] ch ) $.
    ax-mcassr $a |- ( ps [] ( ph [] ch ) ) $.
  $}

  $( <> has unit F. $)
  ${
    pr-mduniti $e |- ps $.
    ax-mduniti $a |- ( ps <> F ) $.
  $}
  ${
    pr-mdunite $e |- ( ps <> F ) $.
    ax-mdunite $a |- ps $.
  $}

  $( <> commutes. $)
  ${
    pr-mdcomm12 $e |- ( ps <> ( ph <> ch ) ) $.
    ax-mdcomm12 $a |- ( ph <> ( ps <> ch ) ) $.
  $}

  $( <> associates. $)
  ${
    pr-mdassl $e |- ( ps <> ( ph <> ch ) ) $.
    ax-mdassl $a |- ( ( ps <> ph ) <> ch ) $.
  $}
  ${
    pr-mdassr $e |- ( ( ps <> ph ) <> ch ) $.
    ax-mdassr $a |- ( ps <> ( ph <> ch ) ) $.
  $}

  $( Two-argument version of ~ ax-mdcomm12 . $)
  ${
    mdcomm.1 $e |- ( ps <> ph ) $.
    mdcomm $p |- ( ph <> ps ) $=
      wph wps wo wps wph wF wph wps wF wph wps wF wps wph wo mdcomm.1
      ax-mduniti ax-mdassr ax-mdcomm12 ax-mdassl ax-mdunite $.
  $}

  $( |_| has unit T. $)
  ${
    pr-acuniti $e |- ps $.
    ax-acuniti $a |- ( ps |_| T ) $.
  $}
  ${
    pr-acunite $e |- ( ps |_| T ) $.
    ax-acunite $a |- ps $.
  $}

  $( |_| commutes. $)
  ${
    pr-accomm $e |- ( ps |_| ph ) $.
    ax-accomm $a |- ( ph |_| ps ) $.
  $}

  $( |_| associates. $)
  ${
    pr-acassl $e |- ( ps |_| ( ph |_| ch ) ) $.
    ax-acassl $a |- ( ( ps |_| ph ) |_| ch ) $.
  $}
  ${
    pr-acassr $e |- ( ( ps |_| ph ) |_| ch ) $.
    ax-acassr $a |- ( ps |_| ( ph |_| ch ) ) $.
  $}

  $( |"| has unit 0. $)
  ${
    pr-aduniti $e |- ps $.
    ax-aduniti $a |- ( ps |"| 0 ) $.
  $}
  ${
    pr-adunite $e |- ( ps |"| 0 ) $.
    ax-adunite $a |- ps $.
  $}

  $( |"| commutes. $)
  ${
    pr-adcomm $e |- ( ps |"| ph ) $.
    ax-adcomm $a |- ( ph |"| ps ) $.
  $}

  $( |"| associates. $)
  ${
    pr-adassl $e |- ( ps |"| ( ph |"| ch ) ) $.
    ax-adassl $a |- ( ( ps |"| ph ) |"| ch ) $.
  $}
  ${
    pr-adassr $e |- ( ( ps |"| ph ) |"| ch ) $.
    ax-adassr $a |- ( ps |"| ( ph |"| ch ) ) $.
  $}

  $( Anything par T can be introduced, as if T were a unit. $)
  ax-parT $a |- ( ps <> T ) $.

  $( As a corollary, T is also a theorem.
     (Contributed by Corbin, 19-May-2019.) $)
  df-T $p |- T $=
    wT wT wF wF ax-parT mdcomm ax-mdunite $.

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        Essential axioms of LK
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  $c ~ $. $( Involution (read:  "not") $)

  $( If ` ph ` is a wff, so is ` ~ ph ` or "not ` ph `." $)
  wi $a wff ~ ph $.

  $c ! $. $( Assert (read: "of course") $)
  $c ? $. $( Question (read: "why not") $)

  wa $a wff ! ph $.
  wq $a wff ? ph $.

  $( We crib from https://johnwickerson.github.io/talks/linearlogic.pdf to
  present a linear version of Gentzen's LK. We fold across |- and dualize as
  needed. $)

  $( Linear logic LEM. This axiom is sometimes called I or AXIOM. $)
  ax-i $a |- ( ph <> ~ ph ) $.

  $( Contraction for why-not. $)
  ${
    pr-contr $e |- ( ? ph <> ? ph ) $.
    ax-contr $a |- ? ph $.
  $}

  $( Weakening for why-not. $)
  ${
    pr-wr $e |- ps $.
    ax-wr $a |- ( ? ph <> ps ) $.
  $}

  $( Additive disjunction has three axioms, one on LHS and two on RHS. The LHS
  axiom dualizes to ~ ax-acr so we omit it. $)
  ${
    pr-adr1 $e |- ps $.
    ax-adr1 $e |- ( ps |"| ph ) $.
  $}
  ${
    pr-adr2 $e |- ps $.
    ax-adr2 $e |- ( ph |"| ps ) $.
  $}

  $( Additive conjunction has three axioms too, two on LHS and one one RHS.
  The LHS axioms dualize to ~ ax-adr1 and ~ ax-adr2 respectively. $)
  ${
    pr1-acr $e |- ps $.
    pr2-acr $e |- ph $.
    ax-acr $a |- ( ps |_| ph ) $.
  $}

  $( Multiplicative disjunction has one axiom on each side. However, the LHS axiom
  dualizes to ~ ax-mcr and the RHS axiom is a restatement of ~ ax-mdassl . $)

  $( Multiplicative conjunction has one axiom on each side. The LHS axiom
  dualizes to ~ ax-mdr . $)
  ${
    pr1-mcr $e |- ( ps <> ph ) $.
    pr2-mcr $e |- ( ch <> th ) $.
    ax-mcr $a |- ( ( ps <> ch ) <> ( ph [] th ) ) $.
  $}

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        De Morgan duality and negation elimination
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  $( Because negation is an involution, and so undoes itself, we dualize the
  premise and axiom names. $)

  $( Double negation. $)
  ${
    pr-dnelim $e |- ps $.
    ax-dnintro $a |- ~ ~ ps $.
  $}
  ${
    pr-dnintro $e |- ~ ~ ps $.
    ax-dnelim $a |- ps $.
  $}

  $( Triple negation. $)
  ${
    notnotnoti.1 $e |- ~ ~ ~ ps $.
    notnotnoti $p |- ~ ps $=
      wps wi notnotnoti.1 ax-dnelim $.
  $}

  $( Dualization of exponentials. $)
  ${
    pr-dnoc $e |- ~ ! ph $.
    ax-dwnn $a |- ? ~ ph $.
  $}
  ${
    pr-dwnn $e |- ? ~ ph $.
    ax-dnoc $a |- ~ ! ph $.
  $}
  ${
    pr-dnwn $e |- ~ ? ph $.
    ax-docn $a |- ! ~ ph $.
  $}
  ${
    pr-docn $e |- ! ~ ph $.
    ax-dnwn $a |- ~ ? ph $.
  $}

  $( Duals for multiplicatives. $)
  ${
    pr-dnmc $e |- ~ ( ps [] ph ) $.
    ax-dmdnn $a |- ( ~ ps <> ~ ph ) $.
  $}
  ${
    pr-dnmd $e |- ~ ( ps <> ph ) $.
    ax-dmcnn $a |- ( ~ ps [] ~ ph ) $.
  $}
  ${
    pr-dmdnn $e |- ( ~ ps <> ~ ph ) $.
    ax-dnmc $a |- ~ ( ps [] ph ) $.
  $}
  ${
    pr-dmcnn $e |- ( ~ ps [] ~ ph ) $.
    ax-dnmd $a |- ~ ( ps <> ph ) $.
  $}

  $( Duals for additives. $)
  ${
    pr-dnac $e |- ~ ( ps |_| ph ) $.
    ax-dadnn $a |- ( ~ ps |"| ~ ph ) $.
  $}
  ${
    pr-dnad $e |- ~ ( ps |"| ph ) $.
    ax-dacnn $a |- ( ~ ps |_| ~ ph ) $.
  $}
  ${
    pr-dadnn $e |- ( ~ ps |"| ~ ph ) $.
    ax-dnac $a |- ~ ( ps |_| ph ) $.
  $}
  ${
    pr-dacnn $e |- ( ~ ps |_| ~ ph ) $.
    ax-dnad $a |- ~ ( ps |"| ph ) $.
  $}

  $( 1 and F are dual. $)
  ${
    dual1F.1 $e |- ~ 1 $.
    dual1F $p |- F $= ? $.
  $}

  $( ~F is a theorem. We use "neg-" to mark these negative results.
     (Contributed by Corbin, 19-May-2019.) $)
  neg-F $p |- ~ F $=
    wF wi wF wi wF wF ax-i mdcomm ax-mdunite $.

  $( 0 and T are dual. $)
  ${
    pr-dual0T $e |- ~ 0 $.
    ax-dual0T $a |- T $.
  $}
  ${
    pr-dualT0 $e |- ~ T $.
    ax-dualT0 $a |- 0 $.
  $}

  $( Multiplicative law of non-contradiction.
     (Contributed by Corbin, 19-May-2019.) $)
  noncontm $p |- ~ ( ps [] ~ ps ) $=
    wps wi wps wps wi ax-i ax-dnmc $.

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        Distributive laws
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  $( "times" distributes over "plus". $)
  ${
    distm $e |- ( ps [] ( ph |_| ch ) ) $.
    ax-distm $a |- ( ( ps [] ph ) |_| ( ps [] ch ) ) $.
  $}

  $( "par" distributes over "with". $)
  ${
    dista $e |- ( ps <> ( ph |"| ch ) ) $.
    ax-dista $a |- ( ( ps <> ph ) |"| ( ps <> ch ) ) $.
  $}

  $( These parens can be associated over. $)
  ${
    lindist.1 $e |- ( ps [] ( ph <> ch ) ) $.
    lindist $p |- ( ( ps [] ph ) <> ch ) $= ? $.
  $}

  $( Half of an isomorphism about of-course. $)
  ${
    expiso.1 $e |- ! ( ph |_| ps ) $.
    expiso $p |- ( ! ph [] ! ps ) $= ? $.
  $}

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        Linear implication
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  $c -o $. $( Lollipop (read:  "implies") $)

  $( If ` ph ` and ` ps ` are wff's, so is ` ( ph -o ps ) ` or " ` ph ` implies
     ` ps ` ."  $)
  wl $a wff ( ph -o ps ) $.

  $( We define linear implication from multiplicative disjunction in order to
  get close to the principle that ` ps -o ph ` and ` ps |- ph ` are
  equivalent. $)
  ${
    pr-impintro $e |- ( ~ ps <> ph ) $.
    df-impintro $a |- ( ps -o ph ) $.
  $}
  ${
    pr-impelim $e |- ( ps -o ph ) $.
    df-impelim $a |- ( ~ ps <> ph ) $.
  $}

  $( Law of contrapositives. $)
  ${
    conpos.1 $e |- ( ps -o ph ) $.
    conpos $p |- ( ~ ph -o ~ ph ) $=
      wph wi wph wi wph wi wi wph wi wph wi ax-i mdcomm df-impintro $.
  $}

  $( Modus ponens for linear implication. $)
  ${
    min $e |- ph $.
    maj $e |- ( ph -o ps ) $.
    ax-mp $a |- ps $.
  $}

  $( The prototypical syllogism. $)
  ${
    syl.1 $e |- ( ph -o ps ) $.
    syl.2 $e |- ( ps -o ch ) $.
    syl $p |- ( ph -o ch ) $= ? $.
  $}

  $( The cut. Gentzen showed famously that this shouldn't have to be an axiom;
  we should figure that out! $)
  ${
    cut.1 $e |- ( ps <> ph ) $.
    cut.2 $e |- ( ~ ph <> ch ) $.
    cut $p |- ( ps <> ch ) $= ? $.
  $}

  $( Law of identity.
     (Contributed by Corbin, 19-May-2019.) $)
  id $p |- ( ph -o ph ) $=
    wph wph wph wi wph wph ax-i mdcomm df-impintro $.

  $( Adding double negation.
     (Contributed by Corbin, 19-May-2019.) $)
  notnot1 $p |- ( ph -o ~ ~ ph ) $=
    wph wi wi wph wph wi ax-i df-impintro $.

  $( Contraposition. $)
  con3 $p |- ( ( ph -o ps ) -o ( ~ ps -o ~ ph ) ) $= ? $.

  $( Elimination of multiplicative conjunction. $)
  simpl $p |- ( ( ph [] ps ) -o ph ) $= ? $.

  $( Elimination of multiplicative conjunction. $)
  simpr $p |- ( ( ph [] ps ) -o ps ) $= ? $.

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        Weakening
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  $( Multiplicative conjunction can be weakened to additive conjunction. $)
  ${
    mcac.1 $e |- ( ph [] ps ) $.
    mcac $p |- ( ph |_| ps ) $= ? $.
  $}

  $( Additive disjunction can be weakened to multiplicative disjunction. $)
  ${
    admd.1 $e |- ( ph |"| ps ) $.
    admd $p |- ( ph <> ps ) $= ? $.
  $}