Consistency as the departing notion, instead of derivability
Jan Burse
Until now I used to define consistency on the
basis of derivability. Namely:
Con(T) :<=> not exists A (T |- A & T |- ~A)
"T is consistent, iff there is no formula A
whereby A can be derived from it and the negation
of A can be derived as well from it".
But there was this funny book, where somebody
did the contrary. Namely he defined:
T |- A :<=> forall B (Con(T u B) -> Con(T u B u A))
"A derives from T, iff for every formula B
such that T u B is consistent, T u B u A is
also consistent."
Is this acceptable?
Bye
translogi
interesting question has more depth than it looks.
But still no
GL (modal logic)
doesn't prove ~[] _|_ neither does it prove []_|_ but the last one can
be added and it is still concistent.
Aatu Koskensilta
> But there was this funny book, where somebody
> did the contrary. Namely he defined:
>
> T |- A :<=> forall B (Con(T u B) -> Con(T u B u A))
>
> "A derives from T, iff for every formula B
> such that T u B is consistent, T u B u A is
> also consistent."
>
> Is this acceptable?
What is the definition of Con(T)?
--
Aatu Koskensilta (aatu.kos...@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophics
Jan Burse
> But still no
>
> GL (modal logic)
> doesn't prove ~[] _|_ neither does it prove []_|_ but the last one can
> be added and it is still concistent.
How about in classical logic. Does this translate to
classical logic?
Bye
Jan Burse
> Jan Burse <janb...@fastmail.fm> writes:
>
>> But there was this funny book, where somebody
>> did the contrary. Namely he defined:
>>
>> T |- A :<=> forall B (Con(T u B) -> Con(T u B u A))
>>
>> "A derives from T, iff for every formula B
>> such that T u B is consistent, T u B u A is
>> also consistent."
>>
>> Is this acceptable?
>
> What is the definition of Con(T)?
>
"T has a model".
Bye
translogi
I presume it does.
I think it follows from (strongly) completeness.
in classical logic all tautologies are provable.
So if A is a tautology it is provable
if A is no tautology then adding it to T (or to T & ~A) leads to
inconsistency.
bye
Jan Burse
> So if A is a tautology it is provable
>
> if A is no tautology then adding it to T (or to T & ~A) leads to
> inconsistency.
>
> bye
What about the non-trivial consequences respective
non-consequences of T? i.e. the formulas A that
somehow relate to T, and would not follow without T.
Bye
translogi
Am not sure what you mean.
But i guess you mean something like
A is consistent with T (A can be true but can also be false, A is
contingent )
in that case
~A is also consistent with T
But T u A u ~A is inconsistent (A u ~A is)
From the first post:
T |- A :<=> forall B (Con(T u B) -> Con(T u B u A))
if B is ~A then
Con(T u ~A) is true
Con(T u ~ A u A)) is false
so
(Con(T u ~A) -> Con(T u ~A u A)) is false
so T doesn't proof A
But maybe you were thinking about something different.
PS it holds for classical logic because it is strongly complete.
(It doesn't hold for intuitionistic logic.)
Jan Burse
> On Jul 1, 2:18 pm, Jan Burse <janbu...@fastmail.fm> wrote:
>> translogi schrieb:
>>
>>> So if A is a tautology it is provable
>>> if A is no tautology then adding it to T (or to T & ~A) leads to
>>> inconsistency.
>>> bye
>> What about the non-trivial consequences respective
>> non-consequences of T? i.e. the formulas A that
>> somehow relate to T, and would not follow without T.
>>
>> Bye
>
> Am not sure what you mean.
>
> But i guess you mean something like
>
> A is consistent with T (A can be true but can also be false, A is
> contingent )
>
> in that case
> ~A is also consistent with T
There is a little drawback in your reasoning,
you cannot follow from:
Con(T u A)
that
Con(T u ~A)
For example if A is undecided in T, then both
T u A and T u ~A are consistent.
What you possibly means, is that from
T |/- A,
you can follow:
Con(T u ~A)
Proof (1):
Take the original definition of |-, then
T |/- A implies, there is M with M |= T
and M |/= A.
Therefore M |= T u ~A. Therefore Con(T u ~A).
> But T u A u ~A is inconsistent (A u ~A is)
>
> From the first post:
> T |- A :<=> forall B (Con(T u B) -> Con(T u B u A))
>
> if B is ~A then
> Con(T u ~A) is true
> Con(T u ~ A u A)) is false
>
> so
> (Con(T u ~A) -> Con(T u ~A u A)) is false
>
> so T doesn't proof A
>
Actually when T |/- A we should have by
definition a witness B with Con(T u B)
& ~Con(T u B u A).
Your witness B=~A is the perfect candidate.
Proof (2):
By (1) we have already shown that Con(T u ~A).
And as you have pointed out ~Con(T u ~A u A).
So in my opinion we have shown one direction
of the implication namely <=.
T |/- A => exists B (Con(T u B) & ~Con(T u B u A))
Or
T |- A <= forall B(Con(T u B) -> Con(T u B u A))
> But maybe you were thinking about something different.
>
> PS it holds for classical logic because it is strongly complete.
> (It doesn't hold for intuitionistic logic.)
What about the other direction =>??
In classsical logic??
Bye
translogi
>
> - Show quoted text -
for
T |- A => forall B(Con(T u B) -> Con(T u B u A))
T |-A implies that Con(T) <=> Con (T u A)
Therefore Con(T u B) <=> Con(T u B u A))
T |-A implies that Con(T) <=> Con (T u A)
can even made stronger
T |- A => forall B(Con(T u B) <=> Con(T u B u A))
if B is consistent with T it is concistend with T u A
if B is inconsistent with T it is inconsistend with T u A
Bye
Jan Burse
> T |- A => forall B(Con(T u B) -> Con(T u B u A))
>
> T |-A implies that Con(T) <=> Con (T u A)
Yep, I see.
Con(T u A) => Con(T) even doesn't need T |- A.
And the forall B is kind of redundant.
Oki, Doki.
Bye
translogi
you are right in
Con(T u A) => Con(T) even doesn't need T |- A
but wrong in
And the forall B is kind of redundant
But maybe it can be rephrased as
T |- A :<=> ~Con(T u ~A)
Also i am still wondering what kind of completeness is neccsary here.
it doesn't hold in weaker that classical logics.
I am very doubtfull in the case of PA.
and it is a quite a meta logical statement.
ect