@user21820 Here is a challenge question that may interest you: Can you tell me why the term electromagnetic force is used as a fundamental force and not broken up into the electric and magnetic forces
The problem is that an invalid proof may not contain any false statements, but rather simply invalid. And the only way to objectively classify them is to use a fixed formal system as reference.
Yes. And in fact, if you study a bit of logic, you will learn the incompleteness theorems, which show that no matter what foundations you choose, if it's not utterly then there will be false statement that cannot be disproven.
So even if an invalid proof makes a false statement we may not be able to disprove it!!
There are countably many sentences over any useful foundational system, so your claims don't make sense. In fact there are some formal systems such as ACF[p] and RCF that are syntactically complete.
But none of them can function as a foundational system, at least in most logicians' views.
Let us be more precise about definable numbers, to avoid common pitfalls.
Suppose we have chosen our favourite foundational system $S$, which is in modern mathematics ZFC. $S$ of course can be implemented by a computer program that will given any input theorem and purported proof will output "ye...
Briefly, you can in a suitable foundational system define the collection of reals, but you cannot individually define most of them, in a certain precise sense, and the usual definitions you find online are usually nonsense.
As far as I know, my post is the only one in a couple of Math SE threads that does it properly.
@Typhon Anything with an "ellipsis" is technically not rigorous (in modern mathematics). As I said before, it's clear to anyone who has basic grasp of first-order logic plus induction. Now in some cases, it is obvious to those in that field how to convert an argument full of ellipses to a rigorous one using induction instead, but in this case doing so would create a more complicated proof than what is actually needed, hence showing conclusively that the asker does not know a proof.
I've read all the existing answers long ago but still feel that none have gotten to the heart of the issue. We obtain mathematical results through a process of reasoning. That reasoning must be logical and enough to convince anyone that our results are correct given our initial assumptions. That ...
One commenter says (and I fully agree):
> I think you're right about the first part: students develop a veritable morass of heuristics and "rules" that somehow "make sense" to them because they get the "right answer" but they cannot explain them at all! − Brendan W. SullivanMay 1 '15 at 18:37
variables = set()
LEM = """If not ( {0} or not {0} ):
If {0}:
{0} or not {0}.
not ( {0} or not {0} ).
False.
not {0}.
{0} or not {0}.
False.
not not ( {0} or not {0} ).
{0} or not {0}."""
def trim(s):
if s == "": return s
hi = len(s)-1
while s[hi] == " ": hi -= 1
return s[:hi+1]
def fragmentation(s):
global variables
depth = 0
curr = ""
fragments = []
for c in s:
if c=="(":
if depth == 0:
if fragments:
for st in trim(curr).split():
if st:
fragments.append(st)
@user21820 I didn't look at your proof
I essentially proved the completeness theorem myself
( P or Q ) and ( Q or R ) and ( R or P ) implies ( P and Q ) or ( Q and R ) or ( R and P )
Result:
If not ( P or not P ):
If P:
P or not P.
not ( P or not P ).
False.
not P.
P or not P.
False.
not not ( P or not P ).
P or not P.
If not ( Q or not Q ):
If Q:
Q or not Q.
not ( Q or not Q ).
False.
not Q.
Q or not Q.
False.
not not ( Q or not Q ).
Q or not Q.
If not ( R or not R ):
If R:
R or not R.
not ( R or not R ).
False.
not R.
R or not R.
False.
not not ( R or not R ).
R or not R.
If P:
If Q:
If R:
P.
Q.
P or Q.
Q.
R.
Q or R.
R.
P.
R or P.
If you want to optimize it, you can do some stuff. For instance, you can prove a (meta) theorem that every implication can be proven with Implies-Elim as the last step.
If not ( A or not A ):
If A:
A or not A.
not ( A or not A ).
False.
not A.
A or not A.
False.
not not ( A or not A ).
A or not A.
If A:
A.
A.
If not A:
A.
False.
not not A.
A or not A.
If not A:
not A.
not A.
A or not A.
but at the same time it's just applying all the templates I gave it
variables = set()
LEM = """If not ( {0} or not {0} ):
If {0}:
{0} or not {0}.
not ( {0} or not {0} ).
False.
not {0}.
{0} or not {0}.
False.
not not ( {0} or not {0} ).
{0} or not {0}."""
def trim(s):
if s == "": return s
hi = len(s)-1
while s[hi] == " ": hi -= 1
return s[:hi+1]
def fragmentation(s):
global variables
depth = 0
curr = ""
fragments = []
for c in s:
if c=="(":
if depth == 0:
if fragments:
for st in trim(curr).split():
if st:
fragments.append(st)
If not ( A or not A ):
If A:
A or not A.
not ( A or not A ).
False.
not A.
A or not A.
False.
not not ( A or not A ).
A or not A.
If not ( B or not B ):
If B:
B or not B.
not ( B or not B ).
False.
not B.
B or not B.
False.
not not ( B or not B ).
B or not B.
If A:
If B:
A.
A.
If not A:
A.
False.
not not A.
B.
If not A:
If not B:
not A.
not not A.
False.
not not B.
B.
not A implies B.
If A:
not A implies B.
A implies ( not A implies B ).
