The 12 systems

[Joseph Knight]

Hi Bruno,

Reading SANE, I don't understand exactly how the 12 logics are obtained from the "basic diamond" of G, G*, V, V*. 

I understand the definitions of know, bet, and correctly bet; so I assume that the 12 logics come by adding certain sentences containing those formulas as axioms to the 4 systems mentioned above? Could you say exactly what the procedure is?

Thanks

[Joseph Knight]

My guess would be p->Bp^p, p->Bp^-B-p, p->Bp^-B-p^p.

[Bruno Marchal]

Hi Joe,

Very busy day, I will answer this evening,

Best,

Bruno

--
You received this message because you are subscribed to the Google Groups "Fabric of Alternate Reality" group.
To unsubscribe from this group and stop receiving emails from it, send an email to foar+uns...@googlegroups.com.
To post to this group, send email to fo...@googlegroups.com.
Visit this group at http://groups.google.com/group/foar.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

http://iridia.ulb.ac.be/~marchal/

[Bruno Marchal]

On 15 Jul 2013, at 04:13, Joseph Knight wrote:

Let us start from G. (which axiomatizes completely what the ideally correct machine can prove about its own provability ability).

G* is what is true about the machine ability (that extends what the machine can prove, for example Dt = ~Bf is true, but the machine cannot prove it)

By Solovay second theorem G* axiomatize completely the logic of that extension. (at the "modal" propositional level).

That is the start. The passage from earth to heaven, in Plotinus, but here it is passage from provable to truth, which is non trivial by Gödel, Löb, Solovay incompleteness theorems.

Then you have the "five" hypostases, or arithmetical points of view. 

p        (the truth)

Bp    (the provable, the logics G and G*)

Bp & p  (the knowable, the logic S4grz)

Bp & Dt   (the observable, the logic, logics Z and Z* )

Bp & Dt & p  (the experienceable, logic X and X*)

I will later, and after I explain more on the relation between G and arithmetic, provides the precise theoem relating the different modal logic of those modalities.

But they exists and are non trivial, and this gives 8 "modal logics", as three of them get two different logics, according to what is true and provable or not.

But, that theory describe a self-referential machine, not necessarily a comp self-referential machine, and comp is axiomatized in arithmetic trhough a restriction of the arithmetical formula to the sigma_1 arithmetical formula (the computable or accessible comp states). This can be shown to be obtained by adding to G the formula p -> Bp.

G is transformed into V, or I also write G1, as "1" is a name for "p -> Bp", ("1" like in sigma_1).

This gives rise to 16 logics. The one above, with p any arithmetical formula, and then the same but starting from G1 instead of G, and thus with p being a sigma_1 arithmetical formula.

Then it can be proved that Z1 is axiomatized by Z + "1", and Z*1 is axiomatized by Z* + "1", but that is not entirely obvious, and it is an open problem for the other arithmetical points of view.

I hope this help, we are far from there, in the current timid beginning. We have not finished computability, and not really begun provability.

Bruno

Thanks

--
You received this message because you are subscribed to the Google Groups "Fabric of Alternate Reality" group.
To unsubscribe from this group and stop receiving emails from it, send an email to foar+uns...@googlegroups.com.
To post to this group, send email to fo...@googlegroups.com.
Visit this group at http://groups.google.com/group/foar.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

http://iridia.ulb.ac.be/~marchal/

[Joseph Knight]

Bruno,

Thanks for your reply. Is there anywhere where the axioms for the 16 logics are written down?

I'm familiar with the motivation for and axioms of G, G*, V, V*, and S4Grz, from reading Boolos, but I haven't seen the axioms for the others written down anywhere, despite seeing them discussed in several of your articles.

Also, what is the theorem you mention that relates them?

You received this message because you are subscribed to a topic in the Google Groups "Fabric of Alternate Reality" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/foar/GQ9l4kUg2uk/unsubscribe.
To unsubscribe from this group and all its topics, send an email to foar+uns...@googlegroups.com.

[Bruno Marchal]

Hi Joseph,

Sorry for answering so late, but my moving has disconnected me for more than a month, at the most hardware level like finding an electrician in summer, installing wires ... and solving problem with companies, etc.

On 25 Jul 2013, at 21:12, Joseph Knight wrote:

Bruno,

Thanks for your reply. Is there anywhere where the axioms for the 16 logics are written down?

It is part of the open problems, but it has been solved for the Z logics (Z, Z1, Z*, Z1*). The decidability of those logics entails the existence of such axiomatics, but to find finite presentation has been solved only for the Z logics, by Eric Vandenbussche 2005:

http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ.html

I'm familiar with the motivation for and axioms of G, G*, V, V*, and S4Grz, from reading Boolos, but I haven't seen the axioms for the others written down anywhere, despite seeing them discussed in several of your articles.

I am problem driven, so I do not choose the axioms for the system, like in provability logic. It is a sort of reverse engineering, and I reason classically, on the problem (defining the first person by the knower using the theaetetus which works thanks to incompleteness. 

Also, what is the theorem you mention that relates them?

I am not sure what you think about. The main theorem is Gödel's second incompleteness, proved by the machine, then the main theorem is Solovay theorem, which relates arithmetical (and some others) interpretation of the G and G* modal logics.

Then incompleteness prevents the (correct) machine from confusing the modalities Bp, Bp & p, Bp & Dt, ... This gives different points of view of a tiny part of arithmetic  about itself. The splitting between G (rationally communicable, provable), and G* (true), is inherited by many intensional variations, like between Bp and Bp & Dt. 

Only arithmetic relates all that.

This remains an invariant for all consistent extensions as long as self-referentially correct. That makes a lot of "Bp" possible.

Taking comp (well understood, or after UDA), and computer science into account, there is a web of dreams (first person experiences) in an already small part of arithmetic (the sigma_1 complete part). The 'theology' is of course concerned between the relation between the dreams (beliefs) and truth.

The splitting between G and G* is a "God" (Arithmetical Truth) given reason for the universal machine or number to get a theology when introspecting enough (to get the *ignorance* and the *many* relative things/experiences). The theology of the machine M is 'just' the truth about M.  Proper theology is truth minus rational believability. It is not empty and (Löbian) universal machines know that it follows from (self) consistency.

Hope this helped a little bit. Ask any question.

Bruno

http://iridia.ulb.ac.be/~marchal/

[Joseph Knight]

On Wednesday, August 28, 2013 12:31:28 PM UTC-5, Bruno Marchal wrote:

Hi Joseph,

Sorry for answering so late, but my moving has disconnected me for more than a month, at the most hardware level like finding an electrician in summer, installing wires ... and solving problem with companies, etc.

Not a problem! In fact I have just moved myself, and experienced similar delays with the internet company. 

 

On 25 Jul 2013, at 21:12, Joseph Knight wrote:

Bruno,

Thanks for your reply. Is there anywhere where the axioms for the 16 logics are written down?

It is part of the open problems, but it has been solved for the Z logics (Z, Z1, Z*, Z1*). The decidability of those logics entails the existence of such axiomatics, but to find finite presentation has been solved only for the Z logics, by Eric Vandenbussche 2005:

http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ.html

So the logics are not specified by a list of axioms but by certain "transformations" on other logics? What are the transformations? They're related to the hypostases, right?

I'll have to go through the axiomatization of the Z's carefully when I have the time. 

Are there semantics for the Z's?

 

I'm familiar with the motivation for and axioms of G, G*, V, V*, and S4Grz, from reading Boolos, but I haven't seen the axioms for the others written down anywhere, despite seeing them discussed in several of your articles.

I am problem driven, so I do not choose the axioms for the system, like in provability logic. It is a sort of reverse engineering, and I reason classically, on the problem (defining the first person by the knower using the theaetetus which works thanks to incompleteness. 

Also, what is the theorem you mention that relates them?

I am not sure what you think about. The main theorem is Gödel's second incompleteness, proved by the machine, then the main theorem is Solovay theorem, which relates arithmetical (and some others) interpretation of the G and G* modal logics.

I was referring to a statement you made in an earlier response: "I will later, and after I explain more on the relation between G and arithmetic, provides the precise theorem relating the different modal logic of those modalities."

[Bruno Marchal]

On 16 Sep 2013, at 14:52, Joseph Knight wrote:

On Wednesday, August 28, 2013 12:31:28 PM UTC-5, Bruno Marchal wrote:

Hi Joseph,

Sorry for answering so late, but my moving has disconnected me for more than a month, at the most hardware level like finding an electrician in summer, installing wires ... and solving problem with companies, etc.

Not a problem! In fact I have just moved myself, and experienced similar delays with the internet company. 

Nothing is easy.

 

On 25 Jul 2013, at 21:12, Joseph Knight wrote:

Bruno,

Thanks for your reply. Is there anywhere where the axioms for the 16 logics are written down?

It is part of the open problems, but it has been solved for the Z logics (Z, Z1, Z*, Z1*). The decidability of those logics entails the existence of such axiomatics, but to find finite presentation has been solved only for the Z logics, by Eric Vandenbussche 2005:

http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ.html

So the logics are not specified by a list of axioms but by certain "transformations" on other logics? What are the transformations? They're related to the hypostases, right?

I'll have to go through the axiomatization of the Z's carefully when I have the time. 

Are there semantics for the Z's?

Yes, in terms of Kripke models for some, Scott-Montague more topological structure for others, and complex sequences of such structure for the logic of the type '*' (featuring the truth about the machine, like G*, Z*, etc.

Now such semantics can have their own interpretation in term of category, or sets, or group. They mathematical objects, so, in some case, we get more "sense" in varying the "set structure" at the base. 

And then, keep in mind you have the basic semantics we start from, the arithmetical interpretation of all formula. 

In a sense, we never live pure mathematics, in fact pure arithmetic. 

Most concept are captured by set of numbers. 

Non arithmetically expressible concept like "true(x)" still defines a precise set of numbers (the set of the Gödel numbers of the true proposition in arithmetic). 

It is something complex and counter-intuitive, so it helps a lot to have the representation theorems (see below).

 

I'm familiar with the motivation for and axioms of G, G*, V, V*, and S4Grz, from reading Boolos, but I haven't seen the axioms for the others written down anywhere, despite seeing them discussed in several of your articles.

I am problem driven, so I do not choose the axioms for the system, like in provability logic. It is a sort of reverse engineering, and I reason classically, on the problem (defining the first person by the knower using the theaetetus which works thanks to incompleteness. 

Also, what is the theorem you mention that relates them?

I am not sure what you think about. The main theorem is Gödel's second incompleteness, proved by the machine, then the main theorem is Solovay theorem, which relates arithmetical (and some others) interpretation of the G and G* modal logics.

I was referring to a statement you made in an earlier response: "I will later, and after I explain more on the relation between G and arithmetic, provides the precise theorem relating the different modal logic of those modalities."

OK. Technically, Solovay theorem is the main theorem, showing that G and G* axiomatize completely and soundly the propositional modal logic of platonist machines' third person self-reference. By Platonist I mean only that the machine believes (even as axioms) 

A v ~A

We can use PA, or ZF, etc. It is Robinson arithmetic + the axioms of induction, but you can take any universal machine having enough knowledge of herself.

A Löbian theory or machine is given by any first order logical specification of a universal (system, machine, number, language, whatever) +  the corresponding induction axioms on its data description.

By limiting the interview on the correct machine, Bp means before and above all that the machine, if chatty enough, and if we are patient enough, the machine will assert p.

Such machines are able to diagonalize, and prove many interesting things about themselves. They have a provability predicate (called Beweisbar by Gödel 1931), and the machine can prove, for all arithmetical formula A,  that  Beweisbar('A') -> Beweisbar('Beweisbar('A')'), but also con('0=0') -> ~beweisbar('con('0=0').

 

The question was: is there a modal logic sound and complete for such formula, true and/or provable by the machine.

Solovay found two of them:

   G, sound and complete (for the arithmetical interpretation) description of the provability and consistency laws she can prove about herself. And

    G*, sound and complete (for the standard model of arithmetic) description of what is true about the provability and consistency of the machine.

That G¨is bigger than G, we knew, by incompleteness. By the second incompleteness theorem Con(t) = ~Beweisbar('~ t') is a typical true, but not provable, self-referential sentence, for that machine.

The representation theorems:

You know modal logic. Syntactically it is just proposition logic + a new symbol [].  It is unary, like the negation ~. so if A is a propositional or modal formula, [] A is an acceptable modal formula. 

Let us define a realization R of the atomic formula of the modal language (that is p1, p2, p3, ...) by a function from {p1, p2, p3, ...} in the set of arithmetical sentences (first order usual axiomatization).

We extend the realization R into a full translation of modal logic recursively by making it commuting with the boolean laws, that is

T(A) = R(A) 

T(A & B) = T(A) & T(B)

T(A v B) = T(A) v T(B)

T(A -> B) = T(A) -> T(B)

T(t) =   0 = 0

Now, this conserves tautologicalness trivially as classical arithmetic obeys classical logic, so the interesting case is:

T([] A) = Beweisbar('A')

In that case Solovay first theorem asserts that  G proves A iff the machines (PM, PA, ZF, etc.) proves, for any realization R, T(A).

Now for the hypostases:

The one I mention by Bp & p, is the one exactly like above, except that you translate, with A any proposition in the language of your machine, []A by Beweisbar('A') & A.

It has been proved by different people that the modal logic S4Grz similarly captures soundly and completely the corresponding logics.

You get the 8 hypostases by substituting above T([] A) = Beweisbar('A'), by, respectively the following:

T([] A) = Beweisbar('A') & A                          (Bp & p, the S4Grz logic, not splitted by proof/truth)

T([] A) = Beweisbar('A') &  Con('0=0')                     (Bp & Dt, the Z logics, which splits proof/truth, like G and G*)

T([] A) = Beweisbar('A') & Con('0=0') & A                (Bp & Dt & p, the X logics, also splits on proof/truth)

To get the "one" logic (G1, Z1, G1*, Z1*, ...), you limit, like a universal dovetailing, the realization R to the sigma_1 arithmetical sentence (the one equivalent to proposition asserting the existence of a number having a verifiable property). (They verify p -> [] p, and model turing universality in arithmetic).

The arithmetical completeness , and the decidability will be inherited, so those logics are well-defined in terms of set of arithmetical, or modal, sentences. 

Z, Z*, Z1, Z1* have been axiomatized, but finite sets of axioms are still missing for S4Grz1 (but here a simple conjecture is that it is p -> []p), and for the X logics.

Sorry if I am too short, or too long, ...

Bruno

http://iridia.ulb.ac.be/~marchal/

[Joseph Knight]

On Mon, Sep 16, 2013 at 11:36 AM, Bruno Marchal <mar...@ulb.ac.be> wrote:

On 16 Sep 2013, at 14:52, Joseph Knight wrote:

On Wednesday, August 28, 2013 12:31:28 PM UTC-5, Bruno Marchal wrote:

Hi Joseph,

Sorry for answering so late, but my moving has disconnected me for more than a month, at the most hardware level like finding an electrician in summer, installing wires ... and solving problem with companies, etc.

Not a problem! In fact I have just moved myself, and experienced similar delays with the internet company. 

Nothing is easy.

 

On 25 Jul 2013, at 21:12, Joseph Knight wrote:

Bruno,

Thanks for your reply. Is there anywhere where the axioms for the 16 logics are written down?

It is part of the open problems, but it has been solved for the Z logics (Z, Z1, Z*, Z1*). The decidability of those logics entails the existence of such axiomatics, but to find finite presentation has been solved only for the Z logics, by Eric Vandenbussche 2005:

http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ.html

So the logics are not specified by a list of axioms but by certain "transformations" on other logics? What are the transformations? They're related to the hypostases, right?

I'll have to go through the axiomatization of the Z's carefully when I have the time. 

Are there semantics for the Z's?

Yes, in terms of Kripke models for some, Scott-Montague more topological structure for others,

Which ones? How do you tell that a logic doesn't have Kripke semantics?

What's the motivation for introducing all of these logics? They all concern provability, consistency, truth, etc. Is the idea to find something "more restrictive" than G/G* for the purposes of finding a measure?

--
Joseph Knight

[Joseph Knight]

So Z comes about as the logic which completely axiomatizes the provable arithmetic realizations where Box(A) translates to Bew("A")^Con("0=0")? I'm confused, as no consistent theory proves Con("0=0").

--
Joseph Knight

[Joseph Knight]

Ah, all this means is that necessitation is not a valid rule in Z. We've definitely left the cozy confines of Kripke's multiverse!

--
Joseph Knight

[Bruno Marchal]

Oops; I missed this post. Sorry.

On 30 Jan 2014, at 07:56, Joseph Knight wrote:

On Mon, Sep 16, 2013 at 11:36 AM, Bruno Marchal <mar...@ulb.ac.be> wrote:

On 16 Sep 2013, at 14:52, Joseph Knight wrote:

On Wednesday, August 28, 2013 12:31:28 PM UTC-5, Bruno Marchal wrote:

Hi Joseph,

Sorry for answering so late, but my moving has disconnected me for more than a month, at the most hardware level like finding an electrician in summer, installing wires ... and solving problem with companies, etc.

Not a problem! In fact I have just moved myself, and experienced similar delays with the internet company. 

Nothing is easy.

 

On 25 Jul 2013, at 21:12, Joseph Knight wrote:

Bruno,

Thanks for your reply. Is there anywhere where the axioms for the 16 logics are written down?

It is part of the open problems, but it has been solved for the Z logics (Z, Z1, Z*, Z1*). The decidability of those logics entails the existence of such axiomatics, but to find finite presentation has been solved only for the Z logics, by Eric Vandenbussche 2005:

http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ.html

So the logics are not specified by a list of axioms but by certain "transformations" on other logics? What are the transformations? They're related to the hypostases, right?

I'll have to go through the axiomatization of the Z's carefully when I have the time. 

Are there semantics for the Z's?

Yes, in terms of Kripke models for some, Scott-Montague more topological structure for others,

Which ones? How do you tell that a logic doesn't have Kripke semantics?

The 8 hypostases are

p   (V)

[]p   []p   (G-----G*)

[]p & p  (S4Grz)

[]p & <>t     []p & <>t  (Z-----Z*)

[]p & <>t & p      []p & <>t & p   (X----X*)

The one on the right, governed by G*, lost the necessitation rule. Z* proves []t, but not [][]t. It lost transitivity too.

Bruno

http://iridia.ulb.ac.be/~marchal/

[Bruno Marchal]

On 13 Mar 2014, at 21:11, Joseph Knight wrote:

So Z comes about as the logic which completely axiomatizes the provable arithmetic realizations where Box(A) translates to Bew("A")^Con("0=0")? I'm confused, as no consistent theory proves Con("0=0").

No consistent theory proves Con("0=0") indeed, but con("0=0") is true (as we limit the interview on sound, and thus consistent, machines). If the machine was proving con("0=0"), she would prove []p equivalent with []p & <>t, and Z would be the same logic as G.

Bruno

For more options, visit https://groups.google.com/d/optout.

http://iridia.ulb.ac.be/~marchal/

[Bruno Marchal]

On 13 Mar 2014, at 21:32, Joseph Knight wrote:

Ah, all this means is that necessitation is not a valid rule in Z.

Indeed.

We've definitely left the cozy confines of Kripke's multiverse!

Yes. It is a good thing, as the Kripke structure does not fit well with the computational neighborhoods, which should have a structure closer to the continuum, like in the UDA.

More on this later probably.

Bruno

For more options, visit https://groups.google.com/d/optout.

http://iridia.ulb.ac.be/~marchal/

[Joseph Knight]

Is there a class of neighborhood (scott montague) models with respect to which Z is known to be sound and complete (like G and the finite, transitive, irreflexive kripke frames)?

Also, how do you prove the correctness of Vandenbussche's axiomatization, is it some modification of Solovay?

What is known about the X logics?

[Bruno Marchal]

On 24 Mar 2014, at 03:18, Joseph Knight wrote:

> Is there a class of neighborhood (scott montague) models with
> respect to which Z is known to be sound and complete (like G and the
> finite, transitive, irreflexive kripke frames)?
>
> Also, how do you prove the correctness of Vandenbussche's
> axiomatization, is it some modification of Solovay?

Not really. Vandenbussche discovered that you can define the G box
with the Z box (and so dually for the lozenge):

if you define [z]A by []A & <>t, like usually, []A can be (re)defined
by [z]A v < z > f. (That equivalence is already provable in K and
simple CPL).

This leads to a simple finite axiomatization of Z. You can consult the
detail from here:

http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ/scan01.html
http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ/scan02.html
http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ/scan03.html

This is rather easy, compared to Solovay theorem, and this solves the
finite axiomatization problem in the positive, for Z, Z1, Z*, Z1*.

Unfortunately the technic cannot be extended to the X, X1, X* and X1*
logic. That' & p" makes things much more complex.

In "conscience and mécanisme" I provide proof of decidability and
axiomatizability (but not the finite one like here) for all the
logics, and show that the non-starred logics have indeed neighborhood
(scott montague) models with respect to which Z is known to be sound.
But give no proof of completeness theorem. One can be extracted as a
consequence of Vandenbussche axiomatization, but it is not that easy
(good question).

http://iridia.ulb.ac.be/~marchal/Vandenbussche/AxiomatisationZ/scan02.html

It shows that Z and G are very close and "bisimulable". The
intensional variance conserves the information. It is rather crazy as
it is opposed on most formula.

I will say more on this in the modal thread on the everything list.
May be I should send the modal summaries here.

>
> What is known about the X logics?

Not much, but they have many similar features, and X1* defines too an
arithmetical quantization. X is to Z, what S4Grz is too G. (same with
1 and *).

More later.

Bruno




http://iridia.ulb.ac.be/~marchal/