You can absolutely formalize proofs using diagonalization arguments on a computer in just the same way you would formalize any other proof. For example here's the Metamath formalization of Cantor's argument that a set cannot be equinumerous to its power set: https://us.metamath.org/mpeuni/canth.html
In mathematics we often use language to talk about a hypothetical function without actually implementing it in any specific programming language. Formal proofs do exactly the same thing in their own formal language.
Although in the case of Cantor's diagonal argument, I don't know in what sense any function involved in that proof would even fail to be implementable in a specific programming language,. Let's say I encode each real number x such that 0 <= x < 1 in my program as a function which takes a positive integer n and returns the n'th digit of x after the decimal point. In Python syntax:
from typing import Callable
# PosInt, Zero and One aren't built-in Python types but just assume they are
Number = Callable[[PosInt], Zero | One]
Sequence = Callable[[PosInt], Number]
The function involved in the diagonalisation argument can then be implemented as follows:
The argument consists of the the observation that whatever sequence you pass as an argument into "diagonalize", the returned number will not be present in the sequence since for every positive integer n, the n'th digit of the returned number will be different from the n'th digit of the n'th number in the sequence, and hence the returned number is distinct from the n'th number in the sequence. Since this holds for every positive integer n, we can conclude that the returned number is distinct from every number in the sequence.
This is just a simple logical argument---it wouldn't be too hard to write it down explicitly as a natural deduction tree where each step is explicitly inferred from previous one using rules like modus ponens, but I'm not going to bother doing that here.
The way I see it, the distinction between = and ≡ isn't really to do with equality having more than one meaning. An "identity" like sin^2 x + cos^2 x ≡ 1 is really just shorthand for "for every real number x, we have sin^2 x + cos^2 x = 1". The equals sign here has the same meaning as in a statement such as "there is a real number x such that sin^2 x + cos^2 x = 1"; the difference is in the surrounding language, and what meaning it assigns to the variable x.
So perhaps rather than just emphasizing the difference between = and ≡ more, it would be better to go further and emphasize the difference between universal and existential quantification more. Quantifiers can be confusing, but I think people also find having two different equals signs confusing; and it wouldn't be necessary to give a full account of predicate logic to high schoolers, I'm thinking more of just informally describing the difference between "for all" and "there exists" and reminding them that a bare variable has no meaning if you don't know what set it ranges over and how it's quantified.
This is just my speculation, I have no experience with mathematical education whatsoever.
"...emphasize the difference between universal and existential quantification more. Quantifiers can be confusing..."
Right, I've uni math also formal logic so I've knowledge of universal and existential quantification, etc. thus an understanding of the issues.
You're right, that stuff's a bit too heavy for highschoolers. Perhaps all that's needed is to be told 'that at times these appear the same but later on you'll need to understand there's a mathematical distinction' then emphasize the difference aspect to drive the point home.
Even though it was a long time ago I mostly recall what the teacher said and whilst he gave a few examples he never emphasized that there was a mathematical difference and that it was an important fact to know. Matters became more ambiguous from our science courses, the use of 'equivalent' was very loose.
I reckon the same or similar should apply to other topics, calculus for example.
I think you misunderstood the parent comment. They're not talking about defining the reals by setting up a mapping where each real number corresponds to a unique natural number. They're talking about defining the reals by setting up a mapping where each real number corresponds to a unique mapping from the natural numbers to {0, 1} (i.e. a unique binary sequence). The set of all binary sequences is isomorphic to the power set of the natural numbers, which is uncountable.
It looks like what Codd means by "psychological features" are features that are (or are intended to) make it easier for users to express what they want to do in the language, as opposed to "logical features" which are what actually enable things to do. It's similar to the concept of "syntactic sugar", I guess. In a well-designed language, there should be a relatively small, theoretically well-understood core of logical features, and the psychological features should be straightforwardly expressible in terms of those logical features. This makes it easier to understand how the language works, which to me, does seem like an important thing for a language (it makes it easier to learn, easier to optimize, easier to add new features to without causing surprising interactions, etc.)
Codd's complaint is that SQL isn't like this, specifically with regard to the psychological feature of being able to nest queries. This was intended to be a more user-friendly alternative to using predicate logic. But instead of designing the nested queries feature as a syntactic sugar layer on top of an underlying predicate logic core, both features were implemented at the "core" level. The result is a hodgepodge language which isn't clearly based on either predicate logic or nested queries alone.
It's still… not the same. In CL (and specially with SBCL), we get compile time (type) errors and warnings at the blink of an eye, when we compile a single function with a keystroke (typically C-c C-c in Slime).
I haven't used CL myself, but it wouldn't surprise me if CL does a better job. Just pointing out that Python is significantly better in this respect than it used to be. In particular, using VS Code with Pylance, I can see type errors highlighted as soon as I write the code---I don't even need to use a keystroke. 24 years ago, I don't think anything like that was possible; the language didn't even support type annotations.
You might be already aware of this, but besides using the backslash, the other way you can allow an expression to span multiple lines in Python is to enclose it in brackets. I find this to be pretty unobtrusive. Often your line break will already be within a pair of brackets anyway.
The "i" sound in "wit" does exist in German and is what is normally indicated by "i" on its own. The long "ee" sound is normally spelt as "ie" in German.
It's not really wrong. There are English accents (such as Received Pronunciation) where an "ee" before an "r" is normally pronounced with an [ɪ] like in "wit". In any case, even if you pronounce the "ee" as something else like [i], "Veert" is probably still the sequence of letters that maximises the likelihood that an English speaker will understand by it something close to the true German pronunciation ([vɪʁt] or [vɪɐt]). "Virt", for example, would be read by most people as [vɜrt] (rhyming with "hurt") which to my ear is further off from the correct pronunciation compared to something like [viət].
In mathematics we often use language to talk about a hypothetical function without actually implementing it in any specific programming language. Formal proofs do exactly the same thing in their own formal language.
Although in the case of Cantor's diagonal argument, I don't know in what sense any function involved in that proof would even fail to be implementable in a specific programming language,. Let's say I encode each real number x such that 0 <= x < 1 in my program as a function which takes a positive integer n and returns the n'th digit of x after the decimal point. In Python syntax:
The function involved in the diagonalisation argument can then be implemented as follows: The argument consists of the the observation that whatever sequence you pass as an argument into "diagonalize", the returned number will not be present in the sequence since for every positive integer n, the n'th digit of the returned number will be different from the n'th digit of the n'th number in the sequence, and hence the returned number is distinct from the n'th number in the sequence. Since this holds for every positive integer n, we can conclude that the returned number is distinct from every number in the sequence.This is just a simple logical argument---it wouldn't be too hard to write it down explicitly as a natural deduction tree where each step is explicitly inferred from previous one using rules like modus ponens, but I'm not going to bother doing that here.