Taktyki dowodowe

do gÓry

Taktyki dowodowe zależą od korelatów semantycznych: korelat dowodzonej formuły (z ewentualnymi rozwinięciami definicyjnymi) i korelat formuły wygenerowanej z dowodu są identyczne.

• wprowadzanie koniunkcji

  α & β
  proof         :: thesis: α & β
    thus α;     :: thesis: β   ==   β & not contradiction
    thus β;     :: thesis: not contradiction
  end;

• założenia

  α implies β
  proof         :: thesis: not (α & not β)
    assume α;   :: thesis: β   ==   β & not contradiction
    thus β;     :: thesis: not contradiction
  end;

  α or β
  proof             :: thesis: not (not α & not β)
    assume not α;   :: thesis: β   ==   β & not contradiction
    thus β;         :: thesis: not contradiction
  end;

• nie wprost

  α
  proof             :: thesis: α
    assume not α;   :: thesis: contradiction
    thus contradiction;   :: thesis: not contradiction
  end;

• przez przypadki

  α
  proof             :: thesis: α
    per cases by ...;   :: β1 or ... or βn
    suppose β1;   :: thesis: α
      thus α;   :: thesis: not contradiction
    end;
    ......
    suppose βn;   :: thesis: α
      thus α;   :: thesis: not contradiction
    end;
  end;

  β1 & α1 or ... or βn & αn
  proof             :: thesis: α
    per cases by ...;   :: β1 or ... or βn
    case β1;   :: thesis: α1
      thus α1;   :: thesis: not contradiction
    end;
    ......
    case βn;   :: thesis: αn
      thus αn;   :: thesis: not contradiction
    end;
  end;

• egzystencjalne

  ex x being Θ st α(x)
  proof
     take y = τ;
     thus α(y);
  end;

  (ex x being Θ st α(x)) implies β
  proof
     given y being Θ such that α(y);
     thus β;
  end;

• ogólne

  for x being Θ holds α(x)
  proof
     let y be Θ;
     thus α(y);
  end;

  for x being Θ st β(x) holds α(x)
  proof
     let y be Θ;
     assume β(y);
     thus α(y);
  end;

• rozwinięcia definicyjne

  τ1,...,τn ρ τn+1,...,τk
  proof             :: thesis: τ1,...,τn ρ τn+1,...,τk
    thus Φ(τ1,...,τk);   :: thesis: not contradiction
  end;

  τ1,...,τn ρ τn+1,...,τk implies α
  proof             :: thesis: not(τ1,...,τn ρ τn+1,...,τk & not α)
    assume Φ(τ1,...,τk);   :: thesis: α
    thus α;          :: thesis: not contradiction
  end;

gdzie Φ(x₁,...,x_k) jest definiensem formuły x₁,...,x_n ρ x_n+1,...,x_k.