Ah ok. So the point is: combining a formal system with a semantics (i.e. assigning an interpretation of the non-logical symbols) results in a formal logic (aka logical system). Then to transform it into a formal theory of something some specific non-logical axioms must be added.
Another example...
Ah ok, so an expression like ##\Gamma \;\vdash\; \varphi## is an instance of a sequent.
As an aside, we can say that a formal system has: a formal language (a set of logical and non-logical symbols taken from the formal language's alphabet), a set of syntax rules for defining wffs within it, a...
I was reading documentation about the soundness and completeness of logic formal systems.
Consider the following $$\vdash_S \phi$$
where ##S## is the proof-system making part the formal system and ##\phi## is a wff (well formed formula) of the formal language. Note the blank on left of the...
Yes exactly. For instance this convention does prescribe to reset to 0 the B's clock at event B2 (i.e. label it as T=0 along B's worldline) when B receives back the light signal emitted at event A1 that encodes T=0 within it. Thus this procedure/convention defines OWSOL as infinite in A -> B...
Just to clarify the point, I drew the following diagram. The base grid ##(x,t)## represents of course the standard inertial coordinate system, in gray the relevant light cones.
At event B1, observer B sends a light signal to observer A. A receives it at A1, resets its own clock to read T=0...
Yes, as far as I can tell the key point is that basically, before the exchange of light signals between observer A and B takes place, it isn't known in advance where the event labeled as 0 by the local clock is located along each of the two observer's worldline.
I believe the topic discussed in this thread is well addressed in R. Penrose's book "The Road to Reality".
In chapter 1, he discusses "mathematical truth" as an objective truth that, let me say, "lives" in the Platonic world. For instance, he offers the example of Fermat's statement, namely...
Yes, the above is the "familiar" 2 x 2 matrix representation for the ##S_z## operator (involving the Pauli z-matrix). By changing the basis vectors used in ##\mathcal H_2## -- without changing the basis-dependent isomorphism ##\phi: \mathcal H_2 \rightarrow \mathbb C^2## -- results in a new...
You mean pick a different orthonormal basis in ##\mathcal H_2## mapping they elements to vectors in ##\mathbb C^2## as prescribed by the "old" basis-dependent isomorphism (i.e. by the isomorphism mapping the previously picked basis's vectors ##\ket{\uparrow}, \ket{\downarrow}## into...
Even though the hyperbolic plane can't be embedded isometrically in 3D Euclidean space, can it be isometrically embedded in three dimensional Minkowski space ?
Just to reiterate what you said. Suppose in the context of ZF set theory (i.e. without throwing in the AC) there was some way to prove that R over Q has no Hamel basis.
Then, since by including the AC axiom (taken as True of course) turning ZF into ZFC can be proven the existence of Hamel basis...
Let me check my understanding. Consider the statement "R over Q doesn't have an Hamel basis". Is it true ? Who knows, what we can say is that with ZF (not including AC) one won't be able to exhibit an Hamel basis for it. In this sense "R over Q doesn’t have an Hamel basis" is consistent with ZF...
Sorry, the point I'm having trouble in understanding is that, I believe, ##\mathbb R_\mathbb Q## for instance either has or has not an Hamel basis, regardless of whether the Axiom of Choice is included in underlying set theory or not.
A different matter is to give a proof of the fact that...