Am I correct in interpreting that your "=T" notation represents "= True"?

Algebra is typically equational. Logic by default is implicational. Dijkstra and Scholten worked out a fully equational logic. It's not widely known outside of the CS community ie logic, philosophy etc. Maybe it's of interest

@Sammich Yes, this has been pretty standard in logic, mathematics, even computer science. britannica.com/topic/truth-value, web.stanford.edu/class/archive/cs/cs103/cs103.1152/lectures/‌​07/…

There is algebra of logic that uses more conventional algebraic notation, see Boolean algebra, for example. But the primary purpose of logic is to relate claims, not to solve equations or derive identities. There is no analog to it in algebra and forcing algebraic notation only makes the enterprise clumsy and encourages wrong associations. Natural deduction systems were specifically introduced to replace earlier Hilbert systems because the latter were too "algebraic" for logic's purposes.

@Rushi Thanks, the Dijkstra/Scholten link is interesting, I wasn't aware of it. Regarding equational vs. implicational, do you mean to say that logic is concerned with causation, while in algebra we treat both sides of the "=" sign as two expressions that are completely interchangeable?

Roughly yes. The principal driver in (traditional) logic is modus ponens/the deduction theorem. D&S replace it with P∨Q≡P

@Conifold Thanks for the links. I see it's quite an extensive topic. Can you, maybe in an answer, give an example where relating claims in algebraic notation is clumsy and encourages wrong associations?

Historical origins.. but consider that the first version of modern logic produced by Boole was very "algebraic".

@Miss_Understands: Simple: Encode False as 0 and True as 1. Then, ≤ encodes implication.

@Miss_Understands Choose either A ⇒ B = A∨B↔A Or else A ⇒ B = A∧B↔B. After that treat the ↔ as = and proceed as school algebra. This is standard lattice theory

It is fairly common to use a valuation function v such that v (P) = 0 expresses that P is false and v (P) = 1 expresses that P is true. Then you could write your argument as v (A → B) = 1; v (A) = 1; therefore, v (B) = 1. But it is rather clumsy. Unless you are trying to make some point about valuations or model theory it is redundant.

The "line under two propositions to indicate the conclusion drawn from them" that you use in the "no english words" linear equation doesn't seem standard in math? Certainly one might use that with a + sign to indicate adding the two equations, but usually in a math assignment I'd write that with a bit of text like "solving the system, we obtain..."? I think a lot of the formal logic symbols are just ways to eliminate that bit of text.

I don't understand. You find it "highly confusing", but this confusion is remedied if you just write "= \top" at the end of each line. Very well, but how is it "highly confusing" to just agree to the convention that the "= \top" is there implicitly?

@Rushi You can also use A ⇒ B = ¬A∨B. It may be a matter of taste, but it looks more "natural", "elementary" to me. Equivalence is then (A ⇒ B) ∧ (B ⇒ A), a derived operation. Similar to (A = B) = (A ≤ B) ∧ (B ≤ A).

That's an important point and it doesn't work!! In logic as object language (eg. digital logic) it's fine. But when we are discussing logic as the formalization/reification of the reasoning process '∨' is useless. It can only be '⇒' — the usual choice for logic. Or '=' — the usual choice for algebra. Iow for object language logic, ¬A∨B works. For metalanguage it doesnt

The key point is that going from P to Q in 'P⇒Q' is information lossy. Going from P to Q in 'P=Q'(you're more likely familiar with it as '⇿' ) is information preserving

For an outsider, anything in math is confusing. It is designed to be understood by someone who has at least learned what its notation stands for. Logic and algebra generally address distinct concepts, so why should the notation be similar?

@DanielAsimov Its reasonable to (ideally) wish for notations which convey the sameness of the same and the difference of the difference. The standard approach to boolean algebra makes (+, ×) in analogy to (∨,∧). This analog is not perfect because: a∧(b∨c) = (a∧b)∨(a∧c) :: a(b+c) = ab + ac. So far it seems to work. BUT a∨(b∧c) = (a∨b) ∧ (a∨c) :: a + bc = (a+b)(a+c) The last is surprising!!

@Rushi Re: "for object language logic, ¬A∨B works. For metalanguage it doesnt" I'm not sure I follow. Can you give an example, perhaps in an answer?

Logic as metalanguage is about driving rational processes. When it becomes superformalized it may look indistinguishable from object language logic. The latter happens archetypally in a computer (note the 'L' in ALUits juxtaposition to 'A'). For the former, one wants a rational process to take one effectively from premises to conclusion (or putative conclusion to trivially true premises ideally T). The connectives in the (meta)proof are therefore ← or →, whereas the objects may be {+,-,*} in arithmetic, {∪, ∩} in set theory. (1/2)

Likewise logic as object-language can use {∧∨} etc and even include →. However at proof level ie metalevel one cannot use {∧∨} as (meta) connectives. The only connectives we know are implies or is-the-same-as ie → or =. If you include in the question something about equational logic (or make a different q) I'll try to answer. (2/2)

Admittedly I am being a bit fast n loose here: strict logicians will assert that the → at meta level should ideally be ⊢. But then it could also be ⊨. So its not clear why we — anyone other than professional logicians — need to get into those weeds!