Explosion and Cut Required

[Mario Carneiro]

On Thu, Jun 16, 2022 at 10:17 AM Joseph Vidal-Rosset <
joseph at vidal-rosset.net> wrote:

> I am aware of the philosophical debates on equivalence and identity, but
> it is indisputable that identity relation is an equivalence relation.
> Therefore, if it has been proved that G is identical to F, every
> sentence that can be formulated in an extensional language (like FOL)
> that is true about G is also true about F, and  reciprocally, if it is
> not true about F is also not true about G. Denying this point would turn
> out to deny simply the principle of Indiscernibility of Identicals and
> that would be absurd.


I'm quite sure that "identity of indiscernibles", applied the way you are
trying to do, is false in Core logic. For example, it is possible to derive
A & ~A |- A in core logic but not F |- A even though |- (A & ~A) <-> F is
derivable. That is, it is not the case that provably equivalent formulas
have all the same (relevant) consequences, which is to some extent the
point: it is considered undesirable that all theorems are equivalent to
true and Core logic is trying to capture a notion of "relevance" that is
simply not preserved by biconditionals.

The technical way this manifests is that is that in the process of applying
the equivalence (A & ~A) <-> F to the hypothesis, we end up at:

F -> (A & ~A), F |- A
and
|- F -> (A & ~A)

both of which are derivable in Core logic, but then we need to use Cut to
combine these, with the result being F |- # instead of F |- A as desired.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220616/42494733/attachment-0001.html>