4

What do you call a statement P which has never been formally proved but all the observations so far verify it?

This question comes from this scenario: some people use a software for work. They often use a specific function. When this function was designed, the developers feared that some errors might occur. However, these errors never occur and workers have used it for years. Of course this function works correctly, because it has never failed. However, no developer has ever taken the time to understand how.

In this example, P is the statement "this function is error free".

  • 6
    A conjecture. See Fermat conjecture prior to 1994. – Mauro ALLEGRANZA Apr 29 '16 at 14:57
  • Informally, you could refer to it as a 'possibility'. – Ask About Monica Apr 29 '16 at 15:06
  • 1
    It's not clear what you're asking now, after your edit. The statement "this has always worked even though we don't know how" is simply true (taking your word for it). So to which statement are you referring when you say "statement that has never been proven"? Do you mean to ask: how do we call a situation in which we don't know how something works? – Eliran Apr 29 '16 at 16:49
  • @EliranH Alberto is describing an induction. "We don't know for sure that the software will continue to work, because we can't prove that it will, but it has always worked in the past so we think it will keep working." The unproven claim is it will keep working. – Era Apr 29 '16 at 17:05
  • What does "this functionality" mean? Don't you mean "this program"? Proof is about propositions/programs, not functionality. – user20153 Apr 29 '16 at 20:02
5

It partly depends on the subject area that the statement falls into, and how it has been supported by facts (e.g. merely not yet contradicted vs. rigorously tested and corroborated). Building off the comments:

You might call this a conjecture if it relates to math or logic, or if it has not been well-corroborated yet.

In science it would be called a hypothesis.

A more general term would be an [epistemic] possibility. Note that it's epistemic because we're talking about evidence and ways we might know something is true; modality isn't really relevant.

Edited after the question:

Your example is interesting because it doesn't seem to fit perfectly into the terms that have been suggested. I would argue that this is a more general case of an inductive claim ("It's always worked in the past, therefore it will continue to work"). You could call the conclusion that it will continue to work an induction. This follows the pattern of referring to a deduced conclusion as a deduction.

Socrates is wise, and Socrates is a man. My deduction is that some men are wise.

Every time I have dropped an apple near the surface of the earth, it has fallen downward. My induction is that it will continue to do so in the future.

This is a slightly unusual usage, I admit, but I think it fits your situation the best.

  • Thanks for the answer. See my edits if you need clarifications. – Alberto Apr 29 '16 at 16:37
  • @Alberto I've edited my answer with another suggestion. – Era Apr 29 '16 at 17:03
  • Thank you @Era, the apple example is exactly what I was trying to say. I think the induction fit my case. – Alberto Apr 29 '16 at 19:06
  • Thank you @Era, I found that "conjecture" was the correct word – Alberto Jan 19 '17 at 15:05
1

Since your question pertained to software, here is a software-related answer: Software that is used in production for years and has not yet failed is called either reliable or mature.

This does not make any assumption about its actual correctness. Both terms only say that it has worked so far under real world usage, not that it has been proven to be correct under any circumstance.

Of course this funcionality is correct, because it has never failed

This is an invalid conclusion. Just because it has not yet failed does not mean it won't in the future. We can't be sure.

There are ways to prove that certain porperties hold under certain conditions, and that is done rigoruously in critical software. Some pieces of software, like the VxWorks OS, are expected to have only one BSOD every 30 years.

1

For the specific software situation you're describing, take a look at Hoare Logic, as discussed, e.g., in https://en.wikipedia.org/wiki/Hoare_logic

In this model, your program's correctness is determined by a collection of Hoare Triples of the form {P}C{Q}, where {P}=preconditions/input, C=your_program, {Q}=postconditions/output. Given input satisfying any of the prescribed preconditions, if your program's output satisfies the corresponding postconditions, then it's "correct".

As a simple example, suppose C=program_to_add_two_numbers. Then one Hoare Triple might be {P}C{Q}, where {P}=both_numbers_to_be_added_are_odd, and {Q}=sum_is_even. Obviously, that one Hoare Triple by itself doesn't establish C's correctness. But an appropriate collection of Hoare Triples usually does. ("Usually" means whenever there exists a collection of Hoare Triples that uniquely, in an if-and-only-if sense, specifies the function : input-->output to be calculated.)

And you might want to check out some of the "See Also" links at the bottom of that wikipedia article for several other models of program correctness. As you might imagine, computer science has devoted lots of rigorous investigation to this subject.

edit: Thanks, @JamesKingsbery Regarding your "term for this concept" remark, yes, I should have explicitly mentioned that you can google the term "program correctness" for lots of additional information.

  • Welcome to Philosophy.SE! Great answer to the question, I didn't know there was a term for this concept! – James Kingsbery May 2 '16 at 14:51
0

As I understand standard usage, a formally provable sentence is a theorem, so "P is a theorem" says that P is true and that the claim that P is true is justifiable by deductive proof. A conjecture is proposed as true, but without formal justification, either deductive or inductive. Empirical claims are never formally provable, so their justifications are either inductive or abductive. This is true even for "laws"; e.g. Ohm's Law is not the sort of thing that can be formally proven. The best we can do is conduct lots of experiments, observe that it never fails to hold, and infer (inductively? abductively?) that is must be true. Then we call it a theory (about the natural world).

I think your use case is fundamentally different. We don't normally call programs theorems, tho we could if we prove them correct. More likely we would call them "certified" or the like. A program that is not formally proven to be correct, but that has never failed, is not really like a an empirical theory, because is is not a natural artifact. Such a program could in principle be proven correct or incorrect, unlike an empirical claim.

I would suggest drawing on engineering rather than logic, and call such programs reliable. This has the advantage of removing the notion of truth, which is a philosophical issue of no relevance to engineering. It also has a nice formal statistical definition that I won't bore you with, and it's related to notions like robustness, since the justification for reliability claims will involve variance: if your code has been running for 10 years without error, but always with the same input, then it may be reliable for that input but you have no idea how robust it is, i.e.whether it is reliable under different conditions.

0

They are called, statements accepted "on faith," "on trust," or "with reservations." An example of this, is the statement - good people go to heaven. The credibility of this statement depends more on the credibility of (trust on) the person making it, than on the statement itself.

With respect to software programs/functions in particular, this is an entirely different thing. A program is made by a person(s), so whether a program will "always" work, under "all possible" conditions, is a function of how thoroughly the programmer covered all such error possibilities and how thoroughly the test department did their job. Obviously, the more thorough these activities were done, the less likely the program will fail. However, the high probability of "human errors" makes it impossible to guarantee that any particular program (or function) will always work under all conditions! Therefore, the statement "this function is error free," needs to be preceded by "so far, this...", to make it a "sensible" statement (a statement that makes sense).

0

A statement that is accepted as true but has never been proven? In mathematics you would call it "incorrectly accepted as true".

Even in software development, where standards will be lower, nobody in their right mind would ever call any software "error-free". You may hear that software has "no known bugs" or "no reported defects".

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.