From: Jan Burse on
Nam Nguyen schrieb:
> I'm not familiar with the deduction theorem, but isn't it true
> {A} |- F /\ ~F would already follow the definition we both stipulated
> above? If the definition of equivalence says that A <-> B iff:
>
> {A} |- B is true _and_ {B} |- A is true

In case you do not yet have the symbol <-> available in your
language, this could be used as a definition for |- A <-> B.

But typically A <-> B is defined as a short hand for
(A -> B) & (B -> A). And then the definition is not necessary,
since it would be a (meta-)theorem.

> Also Part of what I'm not clear below is what you'd mean by
> "{}": what formal system would that be?

Derivation of conclusion B from premisses A1, .., An:

{A1, .., An} |- B

Derivation of conlusion B purely logical, i.e. zero premisses:

{} |- B

But usually {} are not written, so the above would be:

A1, .., An |- B

And:

|- B

Bye
From: jb on
> > above? If the definition of equivalence says that A <-> B iff:
> > {A} |- B is true _and_ {B} |- A is true
> In case you do not yet have the symbol <-> available in your
> language, this could be used as a definition for |- A <-> B.

Well not quite so. This would only deliver a rule where
the equivalence "<->" can be introduced on the right hand
side of the consequence relation "|-". To be complete
we would also need a rule, that says how the equivalence
"<->" can be introduced on the left hand side of the
consequence relation "|-" (*).

So the right hand side rule would be:

G, A |- B
H, B |- A
-------------
G, H |- A <-> B

Now how could the left hand side rule look like? Here is my guess,
there would be two rules for the left hand side:

G |- A
H, B, A |- C
--------------------------
G, H, A <-> B |- C

G |- B
H, B, A |- C
--------------------------
G, H, A <-> B |- C

Right?

(*)
Other schools might require that we exhibit an elimination
rule for the right hand side.