Re: The simple essence of Proof Theoretic Semantics

On 7/2/2026 6:13 PM, olcott wrote:
> On 7/2/2026 4:59 PM, dbush wrote:
>> On 7/2/2026 5:40 PM, olcott wrote:
>>> On 7/2/2026 4:23 PM, dbush wrote:
>>>> On 7/2/2026 5:12 PM, olcott wrote:
>>>>> On 7/2/2026 3:54 PM, dbush wrote:
>>>>>> On 7/2/2026 4:53 PM, olcott wrote:
>>>>>>> On 7/2/2026 2:52 PM, dbush wrote:
>>>>>>>> On 7/2/2026 3:33 PM, olcott wrote:
>>>>>>>>> On 7/2/2026 1:22 PM, dbush wrote:
>>>>>>>>>> On 7/2/2026 2:13 PM, olcott wrote:
>>>>>>>>>>> On 7/2/2026 11:55 AM, dbush wrote:
>>>>>>>>>>>> On 7/2/2026 12:52 PM, olcott wrote:
>>>>>>>>>>>>> On 7/2/2026 11:04 AM, dbush wrote:
>>>>>>>>>>>>>> On 7/2/2026 10:51 AM, olcott wrote:
>>>>>>>>>>>>>>> On 7/2/2026 1:57 AM, Mikko wrote:
>>>>>>>>>>>>>>>> On 02/07/2026 07:03, olcott wrote:
>>>>>>>>>>>>>>>>> On 7/1/2026 11:01 PM, dbush wrote:
>>>>>>>>>>>>>>>>>> On 7/1/2026 11:59 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 7/1/2026 10:43 PM, dbush wrote:
>>>>>>>>>>>>>>>>>>>> On 7/1/2026 11:37 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 10:18 PM, dbush wrote:
>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 11:17 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 10:00 PM, dbush wrote:
>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 10:53 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 9:36 PM, dbush wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 7:37 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 4:15 PM, dbush wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 5:04 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 3:57 PM, dbush wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 4:50 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 3:37 PM, dbush wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 4:29 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 3:13 PM, André G. Isaak wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2026-07-01 13:53, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 2:31 PM, André G. Isaak 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2026-07-01 12:51, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 1:45 PM, André G. Isaak 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 2026-07-01 12:15, dbush wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 7/1/2026 2:01 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The same thing as: "cats are 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> animals" expressed in
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> English has no English meaning 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> in Chinese.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> I didn't ask for an example.  I 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> asked for a definition of what it 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> mean for the truth value of a 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> statement to not exist in a 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> formal system.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> I'm actually not convinced that 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Olcott understands what a 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> definition is. I've frequently 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> asked him for definitions and he 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> invariably responds with an 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> example or an analogy (assuming he 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> responds at all). He doesn't get 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> that examples don't take the place 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> of definitions. Examples can be 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> useful for clarifying definitions, 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> but they aren't particularly 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> useful on their own.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> You want a definition look-it-up.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Until someone publishes an Olcott to 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Standard English dictionary, this 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> isn't really an option.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> True(L, X) ≡ ∃Γ ⊆ BaseFacts(L) (Γ ⊢ 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> X) // copyright Olcott 2018
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> has been updated to this
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> True(L, X):= ∃Γ ⊆ AtomicFacts(L) (Γ ⊢ X)
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> That claims what it means to have the 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> truth value 'true' (or at least it 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> would if you defined AtomicFacts in a 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> coherent way). It doesn't in any way 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> clarify what you think it means for 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> something to not have a truth value.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> André
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> When I define a term hundreds of times 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> and you did
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> not bother to pay attention that is 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> your mistake
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> and your fault.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> You gave no such definition of what it 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> means for the truth value of a statement 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> to not exist in a formal system.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> A valid answer would look something like 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> this:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> "The truth value of a statement does not 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> exist in a formal system when ..."
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Now complete the sentence.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> It is neither provable nor refutable in F.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Good.  So when you say "The truth value of 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> (∀ x, S(x) ≠ x) does not exist in Q", you 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> mean "(∀ x, S(x) ≠ x) is unprovable in Q", 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> which is commonly known.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> So once again, you're saying the same 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> thing as everyone else but using different 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> words.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Not really. It is normally thought of as 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> undecidable
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> meaning that Q is incomplete meaning that Q 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> is deficient.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> False.  It means that there are statements 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> in the language of Q that have *only* an 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> infinite connection to the axioms of the 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> system.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> OK, I verified that.
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The Halting Problem counter-example input 
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> Which starts with the assumption that an 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> algorithm H exists that meets the following 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> requirements:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> Given any algorithm (i.e. a fixed immutable 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> sequence of instructions) X described as <X> 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> with input Y:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> A solution to the halting problem is an 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> algorithm H that computes the following 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> mapping:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> (<X>,Y) maps to 1 if and only if X(Y) halts 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> when executed directly
>>>>>>>>>>>>>>>>>>>>>>>>>>>> (<X>,Y) maps to 0 if and only if X(Y) does 
>>>>>>>>>>>>>>>>>>>>>>>>>>>> not halt when executed directly
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> Sure and we could equally start with the 
>>>>>>>>>>>>>>>>>>>>>>>>>>> requirement
>>>>>>>>>>>>>>>>>>>>>>>>>>> to prove that there exists a natural number > 
>>>>>>>>>>>>>>>>>>>>>>>>>>> 3 and < 2.
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> I really don't see how everyone did not 
>>>>>>>>>>>>>>>>>>>>>>>>>>> immediately see
>>>>>>>>>>>>>>>>>>>>>>>>>>> that the requirement for H to correctly 
>>>>>>>>>>>>>>>>>>>>>>>>>>> report the halt
>>>>>>>>>>>>>>>>>>>>>>>>>>> status of input D that does the opposite of 
>>>>>>>>>>>>>>>>>>>>>>>>>>> whatever H
>>>>>>>>>>>>>>>>>>>>>>>>>>> reports is a moronically stupid requirement 
>>>>>>>>>>>>>>>>>>>>>>>>>>> within the
>>>>>>>>>>>>>>>>>>>>>>>>>>> first five minutes that this requirement was 
>>>>>>>>>>>>>>>>>>>>>>>>>>> made.
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> In other words, you don't understand that if 
>>>>>>>>>>>>>>>>>>>>>>>>>> this was algorithm H:
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> I spent 10,000 hours on it over 22 years.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> And still don't understand that this algorithm:
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> void D(ptr *I)
>>>>>>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>>>>>>>      ptr *X = D;
>>>>>>>>>>>>>>>>>>>>>>>>      ptr *Y = I;
>>>>>>>>>>>>>>>>>>>>>>>>      int result;
>>>>>>>>>>>>>>>>>>>>>>>>      {
>>>>>>>>>>>>>>>>>>>>>>>>          result = 0;
>>>>>>>>>>>>>>>>>>>>>>>>      }
>>>>>>>>>>>>>>>>>>>>>>>>      if (result == 1) {
>>>>>>>>>>>>>>>>>>>>>>>>          while (1);
>>>>>>>>>>>>>>>>>>>>>>>>      }
>>>>>>>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> Is the counter example input to this algorithm:
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> int H(ptr *X, ptr *Y)
>>>>>>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>>>>>>>      int result;
>>>>>>>>>>>>>>>>>>>>>>>>      {
>>>>>>>>>>>>>>>>>>>>>>>>          result = 0;
>>>>>>>>>>>>>>>>>>>>>>>>      }
>>>>>>>>>>>>>>>>>>>>>>>>      return result;
>>>>>>>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> That is just nonsense.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> Thereby proving that you've misunderstood the 
>>>>>>>>>>>>>>>>>>>>>> halting problem for the last 22 years.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> D(D);   // merely halts
>>>>>>>>>>>>>>>>>>>>> H(D,D); // merely returns 0 and never looks at D(D)
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> And algorithm H is wrong about algorithm D because 
>>>>>>>>>>>>>>>>>>>> algorithm D contains a copy of algorithm H and does 
>>>>>>>>>>>>>>>>>>>> the opposite.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> You just don't know jack shit dufus.
>>>>>>>>>>>>>>>>>>> I have been a professional C programmer since 1986.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Says the person that just demonstrated that they don't 
>>>>>>>>>>>>>>>>>> know the difference between an algorithm and a C 
>>>>>>>>>>>>>>>>>> function.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Back to being ignored for trolling again.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Maybe by someone but you are still far from being 
>>>>>>>>>>>>>>>> ignored by everone.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Do you know enough about C to understand that
>>>>>>>>>>>>>>> dbush example was foolish nonsense when proposed
>>>>>>>>>>>>>>> to show the halting problem counter-example?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> It perfectly illustrates an algorithm that attempts to be 
>>>>>>>>>>>>>> a halt decider, 
>>>>>>>>>>>>>
>>>>>>>>>>>>> Ridiculously stupid. Your H does not even look at its input.
>>>>>>>>>>>>
>>>>>>>>>>>> Algorithm H doesn't need to read its inputs in order to map 
>>>>>>>>>>>> all inputs to non-halting.
>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Also your D simply stops running I ran it to verify.
>>>>>>>>>>>>
>>>>>>>>>>>> Verifying that algorithm H doesn't correctly report what 
>>>>>>>>>>>> algorithm D does, as per the design of algorithm D.
>>>>>>>>>>>>
>>>>>>>>
>>>>>>>> Still no reply to this, so I have to assume you agree it's correct.
>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> I am trying to keep liars from killing the
>>>>>>>>>>> whole fucking planet by making truth computable
>>>>>>>>>>
>>>>>>>>>> Which can't be done as proved by Turing / Godel / Tarksi and 
>>>>>>>>>> others.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> By proving the errors in logic I can make
>>>>>>>>> logic into correct reasoning. That most
>>>>>>>>> logic people are a herd of sheep that would
>>>>>>>>> gladly leap off the POE cliff when that is
>>>>>>>>> what their herd accepts makes correcting this
>>>>>>>>> error too fucking difficult.
>>>>>>>>
>>>>>>>> There is no error.  The POE follows from a series of truth 
>>>>>>>> preserving operations 
>>>>>>>
>>>>>>> To say this objectively classical logic is objectively incorrect
>>>>>>> when it diverges from what correct reasoning would be while
>>>>>>> retaining the full English semantics of the terms.
>>>>>>>
>>>>>>> (P ∧ ¬P) ⊢ Q  is ridiculously stupid when we plug English
>>>>>>> sentences in for P and Q and use semantic entailment in English
>>>>>>> as the measure of correct reasoning.
>>>>>>>
>>>>>>>
>>>>>>
>>>>>>
>>>>>> We already did that and you got confused, calling it a mind game 
>>>>>> (see below):
>>>>>>
>>>>> The confusing part is how an intelligent person can
>>>>> accept POE as correct for more than sixty seconds.
>>>>>
>>>>> Every average third grader knows that a contradiction
>>>> States that both a statement and its negation are true.  And if a 
>>>> formal system can reach a contradiction through a series of truth 
>>>> preserving operations from its axioms, that means both statements 
>>>> are proven true.
>>>>
>>>
>>> Every third grader knows that it must have fucked up somewhere.
>>
>> Your intuition fails you.  It just means that the axioms of the system 
>> in question are inconsistent.  And the principle of explosion can be 
>> used to show that an inconsistent system is useless.
>>
> 
> It makes more sense to use the ordinary meaning
> of contradiction:
> 
> When-so-ever two sentences contradict each other
> at least one of them is false.

Whatever you call it, if the axioms of a formal system can prove both X 
and ~X, then the principle of explosion can be used to show that system 
is useless.