Pravidla Přirozené Dedukce

natural-deduction-rules.typ

#import "@preview/curryst:0.4.0": rule, proof-tree

#let proof-box(assumption, conclusion) = box(
  stroke: 0.5pt + black, 
  table(columns: auto, align: center + horizon, stroke: none, assumption, $dots.v$, conclusion)
)

#set page("a4", flipped: true, margin: 10pt)

#align(center + horizon)[
  = Pravidla přirozené dedukce
]

#table(columns: (38%, 64%), stroke: none, align: center + top)[
  == Spojky
  #table(
    columns: (auto, auto, auto),
    inset: 5pt,
    align: horizon + center,
    table.header(
      [Spojka],
      [Zavedeni],
      [Eliminace],
    ),
  
    $and$,
    $ #proof-tree(rule($phi and psi$, $phi$, $psi$ )) "i"and $,
    $
      #proof-tree(rule($phi$, $phi and psi$)) "e"and_1 \
      #proof-tree(rule($psi$, $phi and psi$)) "e"and_2
    $,
  
    $or$,
    $
      #proof-tree(rule($phi or psi$, $phi$ )) "i"or_1 \
    #proof-tree(rule($phi or psi$, $psi$ )) "i"or_2 \
    $,
    $
      #proof-tree(rule($chi$, $phi or psi$, proof-box($phi$, $chi$), proof-box($psi$, $chi$))) "e"or
    $,
  
    $=>$,
    $ #proof-tree(rule($phi => psi$, proof-box($phi$, $psi$))) "i"=> $,
    $ #proof-tree(rule($psi$, $phi$, $phi => psi$, )) "e"=> $,
  
    $<=>$,
    $
      #proof-tree(rule($phi <=> psi$, proof-box($phi$, $psi$), proof-box($psi$, $phi$))) "i"<=>
    $,
    $
      #proof-tree(rule($psi$, $phi$, $phi <=> psi$)) "e"attach(<=>, br: 1) \
      #proof-tree(rule($phi$, $phi <=> psi$, $psi$ )) "e"attach(<=>, br: 2) \
    $,
  
    $not$,
    $ #proof-tree(rule($not phi$, proof-box($phi$, $tack.t$))) "i"not $,
    $ #proof-tree(rule($tack.t$, $phi$, $not phi$)) "e"not $,
  
    $not not$,
    $ "(netřeba)" #proof-tree(rule($not not phi$, $phi$)) "i"not not $,
    $ #proof-tree(rule($phi$, $not not phi$)) "e"not not $,
  
    $tack.t$,
    [není],
    $ #proof-tree(rule($phi$, $tack.t$)) "e"tack.t $,
  
    $tack.b$,
    $ #proof-tree(rule($tack.b$)) "i"tack.b $,
    [není],
  )
][
  == Kvantifikátory
  #table(
    columns: (auto, auto, auto),
    inset: 5pt,
    align: horizon + center,
    table.header(
      [Kvantifikátor],
      [Zavedeni],
      [Eliminace],
    ),
  
    $forall x$,
    $ #proof-tree(rule($forall x phi$, proof-box($x_0$, $phi[x_0\/x]$))) "i"forall x $,
    $
      #proof-tree(rule($phi[t\/x]$, $forall x phi$)) "e"forall x \
    $,
  
    $exists x$,
    $
      #proof-tree(rule($exists x phi$, $phi[t\/x]$ )) "i"exists x
    $,
    $
      #proof-tree(rule($chi$, $exists x phi$, proof-box($x_0: phi[x_0\/x]$, $chi$))) "e"exists x
    $
  )

  == Rovnost
  #table(
    columns: (auto, auto, auto, auto, auto),
    inset: 5pt,
    align: horizon + center,
    table.header(
      [],
      [Zavedení],
      [Eliminace],
      [Symetrie],
      [Transitivita]
    ),

    [Rovnost],
    $ #proof-tree(rule($t = t$)) "i"= $,
    $ #proof-tree(rule($phi[t_2\/x]$, $t_1 = t_2$, $phi[t_1\/x]$)) "e"= $,
    $ #proof-tree(rule($t_2 = t_1$, $t_1 = t_2$)) "sym"= $,
    $ #proof-tree(rule($t_1 = t_3$, $t_1 = t_2$, $t_2 = t_3$)) "trans"= $,
  )

  == Poznámky
  #align(left)[
    Ve všech pravidlech předpokládáme, že substituovaný term je volný pro danou proměnnou v dané formuli. V~používaných termech se nesmí objevovat nedeklarované proměnné.
  ]

  == Pomocná pravidla
  #align(left)[
    Pomocné pravidlo iterace: $"it"$.
  ]

  == Odvozená pravidla
  #align(left)[
    Zákon vyloučeného třetího (law of excluded middle, tertium non datur): $#proof-tree(rule($phi or not phi$)) "LEM"$.
  ]
]