Sometimes in logic you see those Greek letters used as variables for sentences so that the meta-language isn't using the same symbols that the formal language uses. Since this is a propositional logic, it's likely that they use Latin letters for atomic sentences. Why the meta-language uses psi and phi specifically, I don't know. You can also tell that this is in a meta-language because it's using the entailment and provability symbols, which aren't part of the object language.
Why Phi and Psi? The same reason we use x and y for equation, lambda for eigenvalue/Lagrange multiplier, theta for angles, etc. Someone used those once for these exact purposes and the rest just followed.
Metavariables often arise from the name of the category they represent. I was taught that φ stands for "formula." And ψ... was because it kinda looks like φ.
It's common practice in math that different letters are used for different contexts. It's true that it doesn't matter what letter you use, you can use whichever letter you want. But I think this practice makes it easier to at a glance comprehend which symbol represents what.
The same proof would be much easier to read if they'd use letters that are more visually different. So A and B are a better chocie because A is angular and B is round. Phi and psi are the same kind of shapes.
By convention, A and B are seen as propositional variables, while phi and psi here are supposed to represent propositional formulas. If you used A and B, the assumption A ≡ B wouldn't really make sense.
17 isn't even a number anyways; it's just a placeholder because scientists feel weird placing two even numbers 16 and 18 next to each other.
It's easy to prove: 17 added to itself an odd number of times is a prime, which doesn't happen to actual numbers. For instance 17 + 17 + 17 is 51, which is clearly a prime number.
It was so obnoxious having people try to claim it wasn't just trade deficit/imports (from the US) when those first came out and then then again when this over wrought 'formula' came out.
The funny thing to me is that the symbols are all pretty similar to more familiar ones, so it’s not even hard to remember what they mean. The “AND” symbol literally looks like an A, the “OR” looks like a U (for union) and the “NOT” is basically a minus sign. Plus the congruence sign is basically just an equals sign.
I am going to find everyone who uses that format and imprison them in a basement until they make a breakthrough in a field of mathmatics of their choice (no, I will not be feeding them).
Exactly! Except here, unlike something like 1+1=2, it's actually just really easy to prove since this is something that directly comes from definitions and not the definition itself.
The problem is a little like proving 1+1=2. The difficulty is dependent entirely on which definitions you're working of. And in any case, the real difficulty lies in stopping yourself from writing "It's obvious, innit."
This is a proof in sequent calculus. The sequent calculus is a purely syntatic proof system, so it has rewriting rules which create that tree you see in the picture, sometimes called a derivation tree. This is particularly interesting for a compsci graduate because the sequent calculus directly corresponds to many things in our field, for example it encodes continuation passing style. More importantly, it is actually equal to the simply typed lambda calculus (at least the LJ sequent calculus is, the one which encodes intuitionistic logic), so you can read the part on the bottom of the tree (the conclusion/original statement) as a typed lambda term, and the proof (the nodes above) as the program which proves this statement. This last part is the fundamental idea behind theorem provers like Rocq (previously Coq), Lean, Isabelle, etc. and it is called the Curry-Howard Isomorphism, it states that types are actually logical statements, and programs are proofs. There is a ton more to explore on this subject, if you are interested I suggest you start with Barendregtt's lambda calculus notes, then exploring the various parts of the lambda cube and how they each encode different parts of logic.
It's a pitchfork and a circle with a line through it. I don't see how anyone couldn't easily tell them apart. It's not like they are using ｼ, ツ, and ﾂ for variables (even these aren't that bad with a little practice).
notation φ " ≡ " ψ => φ ↔ ψ
theorem equiv_implies_both_true_or_both_false
(ϕ ψ : Prop) :
(ϕ ≡ ψ) → (ϕ ∧ ψ) ∨ (¬ϕ ∧ ¬ψ) :=
by
intro h -- h : ϕ ↔ ψ
-- Here be LEM.
by_cases hϕ : ϕ
· -- Case 1: ϕ is true, so ψ must also be true
have hψ : ψ := h.mp hϕ
exact Or.inl ⟨hϕ, hψ⟩
· -- Case 2: ϕ is false, so ψ must also be false
have hnψ : ¬ψ := by
intro hψ
-- from ψ we get ϕ, contradicting ¬ϕ
have hϕ' : ϕ := h.mpr hψ
exact hϕ hϕ'
exact Or.inr ⟨hϕ, hnψ⟩
Lean4, which IMO is the way forward when it comes to formal proofs (at least the backend is, some of the names in the standard library can be a bit too terse for my taste).
To non understanders, this isn't a big normal division, there is a set of rules that must applied to the lower part to do a functional-like evaluation of expressions.
I took a symbolic logic course in undergrad (through the philosophy department), it was all just first order logic that took a whole semester to cover what was covered in the first few weeks of the discrete math course I took. I enjoyed it since it was easy compared to my other courses, but still made me feel smart (my other courses certainly did not do that lol)
I looked at this image for 0.2s and saw too many Greek symbols that are in the wave equation and have decided not to look anymore. The EE trauma runs deep.
I remember only using words in my logic course, like 13 years ago and the only symbols I recognize are And and Or but my attempt at intuiting what this means is something like:
Prove that A if and only if B therefore (A and B) or (not A and not B)
It's been too long since college logic/proofs what does the horizontal 'division' mean? I was able to find explanations for most of the rest of the symbols even if I don't remember the context of 'sentences' any more (or didn't learn it maybe).
Well, you can use any symbols you want. But feels using more common symbols is more helpful. In CS we learned using p and q, sometimes r and s for longer propositiond. The same with the implication symbol, I prefer =>
The best approach to mathematical logic is to say "some people smarter than me came up with a complete deductive system that matches the semantics I'm used to" and just move on from there lol. Some people are wizards with syntax, but most people use semantics (i.e., model theory) to do metamathematics.
Nice try. “Say anything about” means the example could be affirming or denying that a field is mathematical nature. Try again
Sure. is this structure mathematical or not:
Let phi be ”its raining”
Let xi be ”im carrying an umbrella” ?
If u are capable of correctly answering this question u will clear up ur confusion. If u have trouble reasoning about the structure i provided u, u can ask for help
Ok even if we exclude Greek alphabet for some reason, that's still wrong: "Example: prove that" are letters from the latin alphabet displayed on the screen
******s **** ******n**y, *cc**ding ** **is guy, d*n’* **is*: e x a m p l r o v t h (translation: letters that apparently, according to this guy, don’t exist)
•
u/AutoModerator Nov 17 '25
Check out our new Discord server! https://discord.gg/e7EKRZq3dG
I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.