Definition talk:Pool of Assumptions

There is a big difference between "premises" and "assumptions": the former are the statements that you start with, while assumptions are (usually temporary) statements that you make (which you expect to get discharged) during the course of the proof. --prime mover 18:32, 29 June 2012 (UTC)

The difference is just the difference between:

"Suppose [..]. Then [..]."

and:

"If [..], then [..]."

more accurately:

"[..] holds if [..] are satisfied."

IMHO one should be able to start writing a proof, a posteriori deciding which assumptions need to be considered premises. Premises to me are after the fact. It's like induction proofs: "Hey, let's imagine that this (out of the blue) is the solution - miraculously, we guessed correctly." This does not reflect research; one asks "What do I need to prove [..]?" rather than "What can I prove with [..]" (although sometimes generalisations can be viewed as asking "What can I still prove with only [..]?"). From a historical perspective, I understand your statements, but I feel that we should stress that premises are de facto nothing more than the assumptions that happened not to be discharged. Giving them a status aparte just feels artificial to me. --Lord_Farin 22:33, 29 June 2012 (UTC)

That went so far over my head I didn't hear it whistle. --prime mover 23:30, 29 June 2012 (UTC)

I tried to argue my point that premises are just undischarged assumptions. I don't see why they are special; they only are when you already know what it takes (i.e., what premises) to derive a particular formula/result. To me, such 'after the fact' knowledge shouldn't be imposed to the proof in advance. Hopefully I succeeded in presenting my case in a more accessible phrasing. --Lord_Farin 06:39, 30 June 2012 (UTC)

Completely not, I'm afraid. Okay, so I'm considering a proof as a construct of the form: $P_1, P_2, \ldots, P_n \vdash Q$ where $P_1 \ldots P_n$ are premises. During the course of the proof you will say "Assume $R$" (where $R$ may be some statement form containing atoms of the various $P_k$. In this context, $R$ is an assumption.

Premises are statements which are made at the start of a proof whose truth you accept as being true in the context of the proof. Their truth value is given. I can not understand your point "you already know what premises to derive a formula / result." Well of course you do. You've discovered a truth, that these things being true result in that thing being true, and having done so you package this truth in a structure which says: "From these premises: ... follows this result (or whatever the word is)." As such it is essential to understand which of the statements you make are the ones whose truth values the result depends upon, and those which you (temporarily) assign values to during the course of the argument, in order to establish the truth value of an interim statement.

I'll argue by way of example. In the rule of or-elimination, you are given $P \lor Q$ as a premise. You are given $P \implies R$ as a premise. You are given $Q \implies R$ as a premise. During the course of construction, you assume $P$ as an assumption. From there you deduce that, given that $P \implies R$ is true (a premise), and assuming that $P$ is true (which is why $P$ is an assumption), then you can deduce that if $P$ were true (note the subjunctive form) then $R$ would be true. Similarly, by assuming $Q$ true, you can also show that $R$ would be true. Finally, the structure of the proof itself says that if, by assuming the truth of $P$ you would be able to deduce $R$, and also by assuming the truth of $Q$ you would be able to deduce $R$, then as long as either $P$ or $Q$ is true, (it does not matter which of them is true,) we can be sure that $R$ is true. You have no need to worry about the truth values of either $P$ or $Q$ and (within the confines of the rules of natural deduction they can be discharged, that is, you can forget about them. And not until all your assumptions have been discharged is your proof complete (i.e. valid).

In such a way you can determine whether or not you have finished, by checking that you have discharged all your assumptions. By conflating premises with assumptions you lose this (relative) simplicity of procedure, and it makes it harder work to prove that the only assumptions your proof rests on are the ones you started with - that is, the premises.

On a functional level, you can look at a proof as being a function. Input: $P \lor Q, P \implies R, Q \implies R$. Output: $R$. The inputs are the premises. The output is the result. Except that's abuse of terminology which would make my teachers defecate in their clothing.

If you like, you can of course express $P_1, P_2, \ldots, P_n \vdash Q$ in the form $\vdash \left({P_1 \land P_2 \land \ldots \land P_n}\right) \implies Q$ which has no premises. It is a single conditional statement. The fact that the two forms are equivalent is a result which arises from the natural deduction axioms. This is why I've been feeling a little uneasy about your approach to presenting this subject - there is confusion between (a) the formal-language approach of PropCalc and the natural-deduction approach, and (b) within that formal-language approach, a confusion between the alphabet and syntax of that formal language and the meta-language used to describe operations in that formal language. For a start, $\vdash$ is not a part of the formal-language approach of PropCalc, as the equivalence between $\left({P_1 \land P_2 \land \ldots \land P_n}\right) \implies Q$ and $P_1, P_2, \ldots, P_n \vdash Q$ is exploited instead. It's a valid approach, but it is not the one taken by the exposition of natural deduction provided here (and the basis of most other "non-formal-language" approaches to symbolic logic that I've seen.

These things are subtle and difficult to explain - and I've found what's even more difficult to explain is the fact that such fine distinctions are important.

An example: while $P \dashv \vdash Q$ is equivalent to $P \iff Q$ which in turn is equivalent to $\left({P \land Q}\right) \lor \left({\lnot P \land \lnot Q}\right)$, is it also correct that $\lnot \left({P \dashv \vdash Q}\right)$ is equivalent to $\lnot \left({P \iff Q}\right)$? I would say NO IT IS NOT, because $\lnot \left({P \iff Q}\right)$ specifically means $\left({P \land \lnot Q}\right) \lor \left({\lnot P \land Q}\right)$, whereas $\lnot \left({P \dashv \vdash Q}\right)$ merely means "It is not always the case that the truth of $P$ implies the truth of $Q$ and vice versa." $\lnot \left({P \dashv \vdash Q}\right)$ does not rule out the possibility that $P = Q = \mathrm F$. --prime mover 10:32, 30 June 2012 (UTC)

Here we go battling in essays - I like it. It allows us to delve deeper into the motivations of the other, trying to grasp their paradigms and from there, to their view on all of mathematics. Critical to me is your sentence:

"[...] the only assumptions your proof rests on are the ones you started with - that is, the premises."

acknowledging that premises are assumptions we do before starting the proof proper. In the style propagated by me, any collection of validly constructed tableau proof lines is a proof. Any assumption which hasn't been discharged yet is essential for the conclusion, in the particular tableau used. Of course, simpler, better tableaus with fewer assumptions may exist.

Consider a situation in which you know a set of premises is sufficient to derive a formula. As I understand it, you are disallowing potentially superfluous premises to be discharged, as they are considered genuinely different from assumptions. But this is artificial; in such situations I don't see how it is conveniently possible to investigate the situations with one or more premises discarded, in that it will be required to rewrite the whole proof.

In my mind, the meaning of $p_1\ldots p_n \vdash q$ is: "$p_1\ldots p_n$ provide a means (in natural deduction) to derive $q$". That is why it would be preferable to write $\vdash_{\mathrm{ND}}$ but I haven't found a way to nicely render it. $\vdash$ is not in any way a symbol of PropCalc. It only symbolises that we are able to construct a formal reasoning in ND that the LHS of it entails the RHS. As for the confusion between the formal language and natural deduction, it's not that hard; an analogy again. Formal language says: "Here you have stuff to play around with"; ND says: "These are a set of rules for a particular game with the stuff you got from the language". Any other proof system is in fact a different game. Stressed again, 'my' approach does not implicitly identify $\vdash p \implies q$ and $p \vdash q$.

If we temporarily try to view a proof as a function (or a machine, for that matter), then the axioms say: "Magically, given these machines, you may build this new machine" (except Assumption, which says "Hey, this is a machine; it throws stuff back at you"), and this is what we call a proof line (constructing new machines from old ones). The point is that we have a machine at every line. Some machines require more stuff to operate correctly (input), and magically some machines are able to output the required input for others (which we may call, discharging an assumption). In this analogy, $\vdash$ means: I know a machine that produces RHS from LHS. So $\vdash$ is a metasymbol expressing some knowledge you have attained. On the other hand, $\implies$ is something internal; it corresponds to $\vdash$ through theorems, but this is after the fact, a consequence of the axioms. It is important to note that ND at this point does not assert anything about soundness or completeness (for simplicity, let's assume with respect to boolean interpretations). It is no more than a means to describe a collection of machines operating on the formal language. This is conceptually detached (at this point) from any interpretation in logic and assertions about 'true' or 'false'. As it turns out, these machines, fed with 'true' in all their input positions, produce a 'true' again (under a boolean interpretation) (this is soundness), and conversely, any logically correct inference may be accomplished by a machine (completeness). Although this is the justification for the machines' invention in the first place, they exist even without the context we like to give them.

Finally, coming to the point of premises and assumptions again, having premises is like having certain conceptual 'blocks' or 'stuff' (I realise I am considering mathematics as 'reality' in this analogy, mind you). The (also conceptual) machines turn these into other 'stuff'. Making assumptions is like imagining to have conceptual blocks, and so on. But as we were speaking conceptually anyway, there is not a difference between these.

Thus, as you may not have realised before, in my presentation the formulae before the $\vdash$ are the ones a particular proof depends upon. If one is not satisfied with the machine requiring so much input, a new machine is to be designed which does a better job.

In conclusion, I think your mind is tied up to the boolean interpretation when coming to the ND realms, while I seem to have a more detached, abstract approach to the concept ND. There is value in both, I think. Without your perspective ND wouldn't have been invented in the first place, while through my perspective one can contemplate different 'collections of machines' which lead to different models for PropCalc. But I think that this difference in perspective is at the very core of why we have had this bi-monologue. I hope this sheet of text has managed to turn it into a proper discussion. --Lord_Farin 12:06, 30 June 2012 (UTC)

Reading back on what you started with, the word "modern" jumped out at me. (Please excuse the disconnected and perhaps incoherent nature of my discourse, I'm currently battling with another project at the moment with an insanely slow upload time, completely outside of my control, and so intermittent attention.)

Again, I'm thinking of pre-packaged proofs, those in which the "minimal" premises are used. Your concern is that for any random bag of statements, some may or may not end up having been "depended upon" to provide the conclusion (aah, that's the word I was looking for when I said "result" above). In the "Let's start with these statements and see where they lead us" approach, I agree you can not tell where they go till you get there. But once you've got there, you can look back and say: it depends on this one, it doesn't depend on this one, I pulled this one out of the air (and later discharged it) ..." and so on. I contend that it is at this point one goes back and analyses what one has done so as to say: "... therefore this is a premise, this is an assumption I made, this is irrelevant."

I also concede that if $P_1, P_2, P_3 \vdash Q$ then (assuming no dependency between the various $P$s) $P_1, P_2, P_3, P_4 \vdash Q$ but $P_4$ is not "relevant". This is all covered in the existing analysis of PropCalc in the discourse leading up to the Completeness and Consistency theorems or whatever they are called.

But (and here is where we differ) the historical literature in which ND was originally presented (although not always called that: I'm thinking in particular of the important E.J.Lemmon, if only I can find it in the haystack of books at the left hand side of my desk - my abstract algebra ones are on top at the moment), great care was taken to distinguish between what contributed to a proof and what did not, because his approach (from ND only) also led to the Completeness etc. theorem. And in the course of development of this train of thought (one which I had not completed because I needed a break and never got back to it) the distinction between "premises" and "assumptions" becomes of greater importance than it might.

In short, IMO it's a distinction well worth keeping, even if only to use that distinction in order to be able to present a series of historically-interesting dissertations. If this site wants to be truly worthy and different, the ability to knit together and present all known approaches to a problem is an asset. To take this modernisation approach to its logical conclusion, we would completely dispense with the medieval logic systems which evolved from the Aristotelian approach, which has a charm all its own. And I think that would be a shame.

Finally: if you are prepared to accept a compromise, then mentioning in the appropriate pages that "premises" and "assumptions" are "sort of the same thing, but historically they have been treated as separate - the distinction between them is ..." etc. etc. then feel free to take that approach. --prime mover 12:49, 30 June 2012 (UTC)

To me, historical approaches are among 'all approaches' and so at least deserve some, if not full, documentation. Since the notation is subject to continuous change (some might say, improvement, but I refuse that paradigm) it may be hard, but at least some dissertation in a paragraph on an appropriate page should be admissible. Hopefully I will be able to produce some worthy text on appropriate pages to cover these historical lines. Oh, and sorry for being modern; at the age of 20, the only thing in which I may be old-fashioned is recalling obtaining our first home computer, ISDN internet and the like (resulting in a (some may say paranoid) dislike of so-called 'social media'), as well as some resentment against the current malfunctioning of the government and community. But as for mathematics, the 'modern' approach is all I have currently witnessed. Other stuff demands my attention but I'm sure I will be back next week to continue this exercise, while trying not to think about the hell awaiting in the PredCalc domain... --Lord_Farin 13:20, 30 June 2012 (UTC)

Opposite end of the timeline for me. Most of my mathematical education has been through peering short-sightedly at a series of older and mouldier (sometimes literally) books I've picked up from thrift stores. I taught myself to be an autodidact. --prime mover 14:16, 30 June 2012 (UTC)