we know from Godel that not all true sentences can be shown true in propositional logic. — Leontiskos

From the Wikipedia article on Formalism (Philosophy)
Formalists within a discipline are completely concerned with "the rules of the game," as there is no other external truth that can be achieved beyond those given rules. — RussellA

Therefore, within the proposition "p is true", the expression "is true" is a syncategorematic expression, which adds nothing to the sense of "p". — RussellA

Soundness (if G |- P then G |= P). Proof is straightforward by induction on length of derivation. I don't know who first proved it. — TonesInDeepFreeze

David Hilbert and Wilhelm Ackermann are often credited with formalizing the notion of soundness in their work on formal logic systems in the early 20th century. Their 1928 book "Grundzüge der theoretischen Logik" (Principles of Mathematical Logic) laid the groundwork for formal systems, including the notion that derivations in a formal system should correspond to semantic truths.
However, the soundness theorem is usually associated with Kurt Gödel, who in 1930 proved both the soundness and completeness of first-order logic (predicate logic) as part of his doctoral dissertation. This work demonstrated that if a formula is provable, it is also true in all models, and conversely, if it is true in all models, it is provable. The proof of soundness is typically straightforward compared to the proof of completeness, but both are key results in Gödel's work.

So while Hilbert and Ackermann helped define the formal system, it is Gödel's 1930 work that solidified the formal proof of soundness in the context of first-order logic. — ChatGPT

Not authoritative, of course — Banno

Again, what you have written shows multiple errors in your understanding of formal logic. — Banno

Tones listed some of your errors for your benefit. — Banno

From the Notre Dame review of Irad Khimi's Thinking and Being — RussellA

I’ve been working with some ideas in Irad Kimhi’s Thinking and Being. Much of what he talks about concerns the nature of the relationship between predication and truth-assertion. It occurred to me that “Existence is not a predicate” has some obvious parallels with “Truth is not a predication.” That is, neither existence nor truth add anything, conceptually, to what they appear to be predicating ‛existence’ and ‛truth’ of. I can say “A hundred thalers exist” but this adds nothing to the concept ‛a hundred thalers’; I can say “It is true that there are a hundred thalers on the table” but this adds nothing to the proposition ‛There are a hundred thalers on the table’. — J

All sorts of interesting questions hinge on getting clear about “and”, “or”, “if/IFF”, “can”, “must”, et al. -- well, who knows, maybe we need a better understanding of “on” too. — J

Where it gets bizarre with Kimhi is his further claim that p itself is syncategorematic. You’re right that he regards p as a fact rather than a Fregean complex, but how then is p used? What is the context we need to provide in order to state a relation involving p? I don’t think that, e.g., joining it with q in ‛p & q’ helps. The problem lies in how facts are asserted – how they’re affirmed or denied. — J

I think Kimhi wants to say something more radical – that the context needed to make use of (syncategorematic) ‛p’ has to involve a monistic understanding of what it is to assert. — J

However, the predominant version of combinatorialism finds its origins in Russell's (1918/1919) theory of logical atomism and Wittgenstein's (1921, 1922, 1974) short but enormously influential Tractatus Logico-Philosophicus.

“From the monist point of view, a simple propositional sign displays a possible act of consciousness.” -- the possibility of affirmation or negation. — J

In English we can deny in a manner that does not affirm the negation of any proposition, and this violates the way that propositional logic conceives of the LEM. In fact, going back to flannel’s thread, this shows that a contradiction in English need not take the form (A ^ ~A). In English one can contradict or deny A without affirming ~A. — Leontiskos

(Propositional logic seems to assume, prima facie, not only the commonsensical idea that C is neither A nor B, but also the deeply counterintuitive idea that C is neither ¬A nor ¬B. Usually if C is neither A nor B then it must be both ¬A and ¬B.) — Leontiskos

[For the non-Fregean] The truth-connector is therefore seen as an expression of an operation. In fact, we can speak of truth and falsity operations, which are performed by . . . is true and . . . is false respectively. The assertion “p is true” is the same as “I truly think p.” There is no logical gap between these assertions. By contrast, the assertion “p is false” is not the same as “I truly think not-p.” Thus, truth and falsity operations are not symmetrical. However, they both apply to p and “A thinks p.” It is only in judgments about others that the use of . . . is false is required in addition to negation. — Kimhi, Thinking and Being, 93

I'm glad to hear you're reading Kimhi -- not for the faint of heart! In fact you may find parts of it easier going than I did, due to your background in Aristotle. — J

It may come down to the difference between 'not-X' (negation as an operation within a proposition) and 'It is not the case that (p)' (denial of a proposition) — J

What Kimhi adds to this, in a manner I'm still grappling with, is the unity part: the claim that "the assertion 'p is true' is the same as 'I truly think p'." In general, the role of an act of consciousness in Kimhi's philosophy is what allows him to take a thoroughly monist stance on these matters, but as I've said before, I think he could have done a much clearer job explaining it. — J

[math]\begin{array} {|c|c|}\hline A\,believes\,p. & A\,believes\,p. & A\,believes\,p. \\ \hline p. & Not-p. & A's\,belief\,is\,correct. \\ \hline So\,A's\,belief\,is\,incorrect. & So\,A's\,belief\,is\,correct. & So\,\,p. \\ \hline  \end{array}[/math]

I didn't participate in the thread you refer us to, and I'm not prepared right now to try to take it all in. — J

A similar point can be made with respect to Frege’s use of semantic notions such as “the sense of . . .” and “the reference of . . . ,” namely, insofar as we come to see them as pointing to similarities and differences displayed by the notation, we recognize that they are not predicates, since all predicates are expressible using the notation; hence we come to see them as mere means deployed to communicate the use of the notation to a learner. In the end, the success of this communication requires this realization. One can say, therefore, that Frege’s universalist conception is eliminativist with respect to both semantical and formal-categorical discourse. Note that the very construction of the Begriffsschrift is not in any obvious way internal to the fact-stating discourse, namely, we cannot describe it as the actualization of the capacity of linguistic self-consciousness which is internal to the activity of assertion as such. — Kimhi, Thinking and Being, 91-2

. . .You are appealing to usage, but the etymology and the historical usage point very clearly to logic as an art of reasoning.

They say that one of the best ways to learn something is to teach it. A few weeks ago I looked at your thread which is intended to teach propositional calculus (link). It's no coincidence that in your third substantial post you were already into truth tables. But even in your first substantial post you said, "What we want to do is to examine the relations between these propositions, rather than their contents." It seems to me that it would have been more apt to say that we want to examine the relations that obtain between these propositions based on their content. Relations hold or fail to hold in light of the content of the relata, and this has everything to do with truth.

Now a pedagogue might choose to introduce the rules of logic before introducing the purpose of logic, much like you could teach a child to kick a ball before introducing them to the game of soccer. Of course I am not convinced that this is sound pedagogy. — Leontiskos