A constructive proof to 1+2+3...+n=n(n+1)/2 follows to, known from the school, a recursive algorithm. A non constructive proof to 1+2+3...+n=n(n+1)/2 should define a function: is this statement true or false for any n. If we've got totally true answer, then a non constructive approach proves a constructive one. Though the latter case is a partial algorithm which should not provide answer at all by non constructive way.

Let me add that a "Terminator of the second generation", though being Schwartz the great, is impossible in the frame of any axiomatic logics, even if we can extend a series of cardinal numbers, and without any loss of generality, I should say. New theory - new laws, but these are occupied yet by those from the previous original theory, as we would see some latter. So that the two Cardinals are enough while. Sometimes I like to joke with teachers of logics: a unit interval is of continuum, yes, that's right, and that is that for a unit square - a hyper continuum? Sure, hyper - said nine of ten. Sic! - as Caesaris had said. I like the similar questions, like you posed, when all thoughts are twisted around the interesting problem, maybe unresolved, trying to refer each time to convenient cases from the ordinary life at the kitchen. A great effort is in need to tune the mind in math logics, oh my...

Suppose we have a formal logic L with axiom system having a non-constructive proof for the completeness theorem with respect to a given semantics. Suppose also that we have a formula A which is true in the semantics. Then we have that the following statement is true: “A has a formal proof in L”. A constructive proof of this statement is by showing the formal proof of A in L. A non-constructive proof follows by the completeness theorem for L.

Dear Dimiter, please give your proof interpretation at the substitution A:="Angle trisection is true; an ordinary semantic within any developed formal logics L".

Dear Peter,

.you say:

"One reasons classically about logic of any kind, whether the logic is itself classical or not, when that's what we believe our reality is like. I think only Dummett insisted on constructive meta-reasoning".

In the field of category theory, , in the heart of the geometry, we need to study all important logic (classical, intuitionistic, linear) in each important metatheory (classical, intuitionistic, linear). For example: to study classical logic in a intuitionistic metatheory means simply to study the classical situations that appear working with sheaves.

Dear Dmitry,

probably your notion of constructiv proof is different from the corresponding notion in mathematical logic. That is why I can not see  how your comments are related to the main question. I can not understand also your question directed to me: your statement  "Angle trisection is true; an ordinary semantic within any developed formal logics L" is an informal statement. It is not a formula in a given formal system  with a given formal semantics and a completeness theorem with respect to the semantics. What kind of "proof interpretation" do you mean?

Dimiter, along yours misunderstanding, I can propose a non constructive proof to the mentioned above tri-section problem that, as known, cannot be resolved within a constructive approach: let us compose an angle from three identical sections. Each section, among these three, can be transformed from any non zero angle fi to any nonzero angle psi in the range between 0 and two pi, using a continuous stretching transform f:fi->psi with a rate psi/fi, by virtue of basic theorems of math analysis. That's all in a proof interpret, nothing more.

Dmitry,

again a missunderstanding but from your side. My example is based on several assumptions, namely : (1) to have a formal system F (with a formalized notion of a proof), (2) to have a formal semantics for the system F and (3) - a completeness theorem for F with respect to the semantics with a non-constructive proof (for instance based on the Axiom of choice). Then Let A be a formula in this language which is true in the semantics. Then the statement B=“The formula A has a proof in F” is a meta-theorem for F which follows by the completeness theorem of F and this is a non-constructive proof for B, because the completeness theorem of F has a non-constructive proof. A constructive proof of B is by showing a formal proof of A. So, we have a non-constructive proof for the existence of a constructive proof.

Formal systems satisfying the above assumptions exist , for instance the First-order Logic. Your sentence A is a statement from the ordinary (informal ) mathematics and is not a formula from a formal system with the above requirements.

Dimiter, thanks. I would like to say: "If q has a constructive proof, then the Theorem is true, If q has no a constructive proof, then the Theorem is also true". The Theorem:= a hypothesis proposed by Giancarlo, in a sence - why not, this is true.

If this my understanding is OK, let me to propose you a substitution: q:= "tri-angle problem". I just asking you to provide a chain of conclusions based on your logical scheme for this concrete case, nothing more.