Axioms independence in Rosser system
$begingroup$
In textbook, I see a method to judge axiom independence: Axiom Systems.
One example is in the link, and in this interpretation, R.S1 is not always A, while the other two are A-tautology, so R.S 1 is independence.
And I hope to know if there is some method to find the specific interpretation to make an axiom not always A. I tried to make it for R.S.3 but failed, there are too many choices and when I change one, I need to change many other items.
discrete-mathematics logic
$endgroup$
add a comment |
$begingroup$
In textbook, I see a method to judge axiom independence: Axiom Systems.
One example is in the link, and in this interpretation, R.S1 is not always A, while the other two are A-tautology, so R.S 1 is independence.
And I hope to know if there is some method to find the specific interpretation to make an axiom not always A. I tried to make it for R.S.3 but failed, there are too many choices and when I change one, I need to change many other items.
discrete-mathematics logic
$endgroup$
add a comment |
$begingroup$
In textbook, I see a method to judge axiom independence: Axiom Systems.
One example is in the link, and in this interpretation, R.S1 is not always A, while the other two are A-tautology, so R.S 1 is independence.
And I hope to know if there is some method to find the specific interpretation to make an axiom not always A. I tried to make it for R.S.3 but failed, there are too many choices and when I change one, I need to change many other items.
discrete-mathematics logic
$endgroup$
In textbook, I see a method to judge axiom independence: Axiom Systems.
One example is in the link, and in this interpretation, R.S1 is not always A, while the other two are A-tautology, so R.S 1 is independence.
And I hope to know if there is some method to find the specific interpretation to make an axiom not always A. I tried to make it for R.S.3 but failed, there are too many choices and when I change one, I need to change many other items.
discrete-mathematics logic
discrete-mathematics logic
asked Jan 15 at 12:09
My_LuluMy_Lulu
62
62
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Before I answer your actual question, I first would like to point out that having R.S.1 not being an A-tautology, while the others are, does not immediately make R.S.1 independent from the others: you also need to verify that using the inference rule(s) as provided by the axiom system under consideration, you can only infer A-tautologies from other A-tautologies. For example, if your only inference rules is Modus Ponens, then you need to verify that whenever $P rightarrow Q$ and $P$ have the value of $A$, then $Q$ has the value of $A$ as well.
Ok, now to your question: Unfortunately, it is indeed not always easy to find an interpretation that works for your purposes, and often you have to do a good bit of trial and error. After you have tried a few things, though, you typically do get a sense of direction as to what such an interpretation would have to look like (and, some values of the interpretation will have to be forced, especially given the necessary nature of the inference rules as I stated in the first point). And, when you get close, you know where it still fails, and sometimes you can just make a small correction to make it fully work.
But no, I don't know of any algorithm that will automatically and quickly generate an interpretation that will work. However, if you have some programming skills, you could write a program to just brute-force the whole space of possible interpretations.
One more thing to note, though. It is possible to find a 'non-standard' interpretations that is still only $2$-valued ... but in my experience that doesn't happen too often. So, typically you'll have to work with a $3$-valued system, and typically there is one of those. However, it is also possible that the only interpretations that will work need more than $3$ values, so now you'll need $4$ or $5$ or ... And again, as far as I can tell, there is really nothing that would systematically be able to predict for you how many values you need.
Hope this helps. Good luck!
$endgroup$
$begingroup$
Thanks for your guidance! I wrote a program to calculate it, and if I didn't make it wrong, the table for ∧ is: A A A; A B C; A C C; B A C; B B C; B C A; C A C; C B C; C C C. The ┐ remains the same as the textbook: A C; B B; C A. I'd check it tomorrow.
$endgroup$
– My_Lulu
Jan 15 at 16:38
$begingroup$
@My_Lulu Unfortunately that doesn't quite work. The inference rule says that you can infer $psi$ from $neg ( varphi land neg psi)$ and $varphi$. Now note that if $varphi$ has the value $A$, and $psi$ has the value $B$, then $neg ( varphi land neg psi)$ and $varphi$ both have value $A$, but $psi$ has value $B$. This means that it becomes possible to derive a statement that is not an $A$-tautology from two statements that are $A$-tautologies, and clearly that's not what you want: you want to show that from $A$-tautologies, you can only infer other $A$-tautologies. Do you see why?
$endgroup$
– Bram28
Jan 15 at 18:06
$begingroup$
@My_Lulu Fortunately, this is one of those cases where you're almost there ... do you see how you need to make one small change to the definition of the $land$ to make it work?
$endgroup$
– Bram28
Jan 15 at 18:15
$begingroup$
Thanks a lot for checking! I make two changes to ∧:A B A and B C B. So the definition now is: A A A; A B A; A C C; B A C; B B C; B C B; C A C; C B C; C C C.
$endgroup$
– My_Lulu
Jan 16 at 2:54
$begingroup$
@My_Lulu I'd have to check to verify that .... but I believe all you needed to change was to have A B A instead of A B C. Good work!
$endgroup$
– Bram28
Jan 16 at 3:17
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3074357%2faxioms-independence-in-rosser-system%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Before I answer your actual question, I first would like to point out that having R.S.1 not being an A-tautology, while the others are, does not immediately make R.S.1 independent from the others: you also need to verify that using the inference rule(s) as provided by the axiom system under consideration, you can only infer A-tautologies from other A-tautologies. For example, if your only inference rules is Modus Ponens, then you need to verify that whenever $P rightarrow Q$ and $P$ have the value of $A$, then $Q$ has the value of $A$ as well.
Ok, now to your question: Unfortunately, it is indeed not always easy to find an interpretation that works for your purposes, and often you have to do a good bit of trial and error. After you have tried a few things, though, you typically do get a sense of direction as to what such an interpretation would have to look like (and, some values of the interpretation will have to be forced, especially given the necessary nature of the inference rules as I stated in the first point). And, when you get close, you know where it still fails, and sometimes you can just make a small correction to make it fully work.
But no, I don't know of any algorithm that will automatically and quickly generate an interpretation that will work. However, if you have some programming skills, you could write a program to just brute-force the whole space of possible interpretations.
One more thing to note, though. It is possible to find a 'non-standard' interpretations that is still only $2$-valued ... but in my experience that doesn't happen too often. So, typically you'll have to work with a $3$-valued system, and typically there is one of those. However, it is also possible that the only interpretations that will work need more than $3$ values, so now you'll need $4$ or $5$ or ... And again, as far as I can tell, there is really nothing that would systematically be able to predict for you how many values you need.
Hope this helps. Good luck!
$endgroup$
$begingroup$
Thanks for your guidance! I wrote a program to calculate it, and if I didn't make it wrong, the table for ∧ is: A A A; A B C; A C C; B A C; B B C; B C A; C A C; C B C; C C C. The ┐ remains the same as the textbook: A C; B B; C A. I'd check it tomorrow.
$endgroup$
– My_Lulu
Jan 15 at 16:38
$begingroup$
@My_Lulu Unfortunately that doesn't quite work. The inference rule says that you can infer $psi$ from $neg ( varphi land neg psi)$ and $varphi$. Now note that if $varphi$ has the value $A$, and $psi$ has the value $B$, then $neg ( varphi land neg psi)$ and $varphi$ both have value $A$, but $psi$ has value $B$. This means that it becomes possible to derive a statement that is not an $A$-tautology from two statements that are $A$-tautologies, and clearly that's not what you want: you want to show that from $A$-tautologies, you can only infer other $A$-tautologies. Do you see why?
$endgroup$
– Bram28
Jan 15 at 18:06
$begingroup$
@My_Lulu Fortunately, this is one of those cases where you're almost there ... do you see how you need to make one small change to the definition of the $land$ to make it work?
$endgroup$
– Bram28
Jan 15 at 18:15
$begingroup$
Thanks a lot for checking! I make two changes to ∧:A B A and B C B. So the definition now is: A A A; A B A; A C C; B A C; B B C; B C B; C A C; C B C; C C C.
$endgroup$
– My_Lulu
Jan 16 at 2:54
$begingroup$
@My_Lulu I'd have to check to verify that .... but I believe all you needed to change was to have A B A instead of A B C. Good work!
$endgroup$
– Bram28
Jan 16 at 3:17
add a comment |
$begingroup$
Before I answer your actual question, I first would like to point out that having R.S.1 not being an A-tautology, while the others are, does not immediately make R.S.1 independent from the others: you also need to verify that using the inference rule(s) as provided by the axiom system under consideration, you can only infer A-tautologies from other A-tautologies. For example, if your only inference rules is Modus Ponens, then you need to verify that whenever $P rightarrow Q$ and $P$ have the value of $A$, then $Q$ has the value of $A$ as well.
Ok, now to your question: Unfortunately, it is indeed not always easy to find an interpretation that works for your purposes, and often you have to do a good bit of trial and error. After you have tried a few things, though, you typically do get a sense of direction as to what such an interpretation would have to look like (and, some values of the interpretation will have to be forced, especially given the necessary nature of the inference rules as I stated in the first point). And, when you get close, you know where it still fails, and sometimes you can just make a small correction to make it fully work.
But no, I don't know of any algorithm that will automatically and quickly generate an interpretation that will work. However, if you have some programming skills, you could write a program to just brute-force the whole space of possible interpretations.
One more thing to note, though. It is possible to find a 'non-standard' interpretations that is still only $2$-valued ... but in my experience that doesn't happen too often. So, typically you'll have to work with a $3$-valued system, and typically there is one of those. However, it is also possible that the only interpretations that will work need more than $3$ values, so now you'll need $4$ or $5$ or ... And again, as far as I can tell, there is really nothing that would systematically be able to predict for you how many values you need.
Hope this helps. Good luck!
$endgroup$
$begingroup$
Thanks for your guidance! I wrote a program to calculate it, and if I didn't make it wrong, the table for ∧ is: A A A; A B C; A C C; B A C; B B C; B C A; C A C; C B C; C C C. The ┐ remains the same as the textbook: A C; B B; C A. I'd check it tomorrow.
$endgroup$
– My_Lulu
Jan 15 at 16:38
$begingroup$
@My_Lulu Unfortunately that doesn't quite work. The inference rule says that you can infer $psi$ from $neg ( varphi land neg psi)$ and $varphi$. Now note that if $varphi$ has the value $A$, and $psi$ has the value $B$, then $neg ( varphi land neg psi)$ and $varphi$ both have value $A$, but $psi$ has value $B$. This means that it becomes possible to derive a statement that is not an $A$-tautology from two statements that are $A$-tautologies, and clearly that's not what you want: you want to show that from $A$-tautologies, you can only infer other $A$-tautologies. Do you see why?
$endgroup$
– Bram28
Jan 15 at 18:06
$begingroup$
@My_Lulu Fortunately, this is one of those cases where you're almost there ... do you see how you need to make one small change to the definition of the $land$ to make it work?
$endgroup$
– Bram28
Jan 15 at 18:15
$begingroup$
Thanks a lot for checking! I make two changes to ∧:A B A and B C B. So the definition now is: A A A; A B A; A C C; B A C; B B C; B C B; C A C; C B C; C C C.
$endgroup$
– My_Lulu
Jan 16 at 2:54
$begingroup$
@My_Lulu I'd have to check to verify that .... but I believe all you needed to change was to have A B A instead of A B C. Good work!
$endgroup$
– Bram28
Jan 16 at 3:17
add a comment |
$begingroup$
Before I answer your actual question, I first would like to point out that having R.S.1 not being an A-tautology, while the others are, does not immediately make R.S.1 independent from the others: you also need to verify that using the inference rule(s) as provided by the axiom system under consideration, you can only infer A-tautologies from other A-tautologies. For example, if your only inference rules is Modus Ponens, then you need to verify that whenever $P rightarrow Q$ and $P$ have the value of $A$, then $Q$ has the value of $A$ as well.
Ok, now to your question: Unfortunately, it is indeed not always easy to find an interpretation that works for your purposes, and often you have to do a good bit of trial and error. After you have tried a few things, though, you typically do get a sense of direction as to what such an interpretation would have to look like (and, some values of the interpretation will have to be forced, especially given the necessary nature of the inference rules as I stated in the first point). And, when you get close, you know where it still fails, and sometimes you can just make a small correction to make it fully work.
But no, I don't know of any algorithm that will automatically and quickly generate an interpretation that will work. However, if you have some programming skills, you could write a program to just brute-force the whole space of possible interpretations.
One more thing to note, though. It is possible to find a 'non-standard' interpretations that is still only $2$-valued ... but in my experience that doesn't happen too often. So, typically you'll have to work with a $3$-valued system, and typically there is one of those. However, it is also possible that the only interpretations that will work need more than $3$ values, so now you'll need $4$ or $5$ or ... And again, as far as I can tell, there is really nothing that would systematically be able to predict for you how many values you need.
Hope this helps. Good luck!
$endgroup$
Before I answer your actual question, I first would like to point out that having R.S.1 not being an A-tautology, while the others are, does not immediately make R.S.1 independent from the others: you also need to verify that using the inference rule(s) as provided by the axiom system under consideration, you can only infer A-tautologies from other A-tautologies. For example, if your only inference rules is Modus Ponens, then you need to verify that whenever $P rightarrow Q$ and $P$ have the value of $A$, then $Q$ has the value of $A$ as well.
Ok, now to your question: Unfortunately, it is indeed not always easy to find an interpretation that works for your purposes, and often you have to do a good bit of trial and error. After you have tried a few things, though, you typically do get a sense of direction as to what such an interpretation would have to look like (and, some values of the interpretation will have to be forced, especially given the necessary nature of the inference rules as I stated in the first point). And, when you get close, you know where it still fails, and sometimes you can just make a small correction to make it fully work.
But no, I don't know of any algorithm that will automatically and quickly generate an interpretation that will work. However, if you have some programming skills, you could write a program to just brute-force the whole space of possible interpretations.
One more thing to note, though. It is possible to find a 'non-standard' interpretations that is still only $2$-valued ... but in my experience that doesn't happen too often. So, typically you'll have to work with a $3$-valued system, and typically there is one of those. However, it is also possible that the only interpretations that will work need more than $3$ values, so now you'll need $4$ or $5$ or ... And again, as far as I can tell, there is really nothing that would systematically be able to predict for you how many values you need.
Hope this helps. Good luck!
answered Jan 15 at 13:54
Bram28Bram28
62.9k44793
62.9k44793
$begingroup$
Thanks for your guidance! I wrote a program to calculate it, and if I didn't make it wrong, the table for ∧ is: A A A; A B C; A C C; B A C; B B C; B C A; C A C; C B C; C C C. The ┐ remains the same as the textbook: A C; B B; C A. I'd check it tomorrow.
$endgroup$
– My_Lulu
Jan 15 at 16:38
$begingroup$
@My_Lulu Unfortunately that doesn't quite work. The inference rule says that you can infer $psi$ from $neg ( varphi land neg psi)$ and $varphi$. Now note that if $varphi$ has the value $A$, and $psi$ has the value $B$, then $neg ( varphi land neg psi)$ and $varphi$ both have value $A$, but $psi$ has value $B$. This means that it becomes possible to derive a statement that is not an $A$-tautology from two statements that are $A$-tautologies, and clearly that's not what you want: you want to show that from $A$-tautologies, you can only infer other $A$-tautologies. Do you see why?
$endgroup$
– Bram28
Jan 15 at 18:06
$begingroup$
@My_Lulu Fortunately, this is one of those cases where you're almost there ... do you see how you need to make one small change to the definition of the $land$ to make it work?
$endgroup$
– Bram28
Jan 15 at 18:15
$begingroup$
Thanks a lot for checking! I make two changes to ∧:A B A and B C B. So the definition now is: A A A; A B A; A C C; B A C; B B C; B C B; C A C; C B C; C C C.
$endgroup$
– My_Lulu
Jan 16 at 2:54
$begingroup$
@My_Lulu I'd have to check to verify that .... but I believe all you needed to change was to have A B A instead of A B C. Good work!
$endgroup$
– Bram28
Jan 16 at 3:17
add a comment |
$begingroup$
Thanks for your guidance! I wrote a program to calculate it, and if I didn't make it wrong, the table for ∧ is: A A A; A B C; A C C; B A C; B B C; B C A; C A C; C B C; C C C. The ┐ remains the same as the textbook: A C; B B; C A. I'd check it tomorrow.
$endgroup$
– My_Lulu
Jan 15 at 16:38
$begingroup$
@My_Lulu Unfortunately that doesn't quite work. The inference rule says that you can infer $psi$ from $neg ( varphi land neg psi)$ and $varphi$. Now note that if $varphi$ has the value $A$, and $psi$ has the value $B$, then $neg ( varphi land neg psi)$ and $varphi$ both have value $A$, but $psi$ has value $B$. This means that it becomes possible to derive a statement that is not an $A$-tautology from two statements that are $A$-tautologies, and clearly that's not what you want: you want to show that from $A$-tautologies, you can only infer other $A$-tautologies. Do you see why?
$endgroup$
– Bram28
Jan 15 at 18:06
$begingroup$
@My_Lulu Fortunately, this is one of those cases where you're almost there ... do you see how you need to make one small change to the definition of the $land$ to make it work?
$endgroup$
– Bram28
Jan 15 at 18:15
$begingroup$
Thanks a lot for checking! I make two changes to ∧:A B A and B C B. So the definition now is: A A A; A B A; A C C; B A C; B B C; B C B; C A C; C B C; C C C.
$endgroup$
– My_Lulu
Jan 16 at 2:54
$begingroup$
@My_Lulu I'd have to check to verify that .... but I believe all you needed to change was to have A B A instead of A B C. Good work!
$endgroup$
– Bram28
Jan 16 at 3:17
$begingroup$
Thanks for your guidance! I wrote a program to calculate it, and if I didn't make it wrong, the table for ∧ is: A A A; A B C; A C C; B A C; B B C; B C A; C A C; C B C; C C C. The ┐ remains the same as the textbook: A C; B B; C A. I'd check it tomorrow.
$endgroup$
– My_Lulu
Jan 15 at 16:38
$begingroup$
Thanks for your guidance! I wrote a program to calculate it, and if I didn't make it wrong, the table for ∧ is: A A A; A B C; A C C; B A C; B B C; B C A; C A C; C B C; C C C. The ┐ remains the same as the textbook: A C; B B; C A. I'd check it tomorrow.
$endgroup$
– My_Lulu
Jan 15 at 16:38
$begingroup$
@My_Lulu Unfortunately that doesn't quite work. The inference rule says that you can infer $psi$ from $neg ( varphi land neg psi)$ and $varphi$. Now note that if $varphi$ has the value $A$, and $psi$ has the value $B$, then $neg ( varphi land neg psi)$ and $varphi$ both have value $A$, but $psi$ has value $B$. This means that it becomes possible to derive a statement that is not an $A$-tautology from two statements that are $A$-tautologies, and clearly that's not what you want: you want to show that from $A$-tautologies, you can only infer other $A$-tautologies. Do you see why?
$endgroup$
– Bram28
Jan 15 at 18:06
$begingroup$
@My_Lulu Unfortunately that doesn't quite work. The inference rule says that you can infer $psi$ from $neg ( varphi land neg psi)$ and $varphi$. Now note that if $varphi$ has the value $A$, and $psi$ has the value $B$, then $neg ( varphi land neg psi)$ and $varphi$ both have value $A$, but $psi$ has value $B$. This means that it becomes possible to derive a statement that is not an $A$-tautology from two statements that are $A$-tautologies, and clearly that's not what you want: you want to show that from $A$-tautologies, you can only infer other $A$-tautologies. Do you see why?
$endgroup$
– Bram28
Jan 15 at 18:06
$begingroup$
@My_Lulu Fortunately, this is one of those cases where you're almost there ... do you see how you need to make one small change to the definition of the $land$ to make it work?
$endgroup$
– Bram28
Jan 15 at 18:15
$begingroup$
@My_Lulu Fortunately, this is one of those cases where you're almost there ... do you see how you need to make one small change to the definition of the $land$ to make it work?
$endgroup$
– Bram28
Jan 15 at 18:15
$begingroup$
Thanks a lot for checking! I make two changes to ∧:A B A and B C B. So the definition now is: A A A; A B A; A C C; B A C; B B C; B C B; C A C; C B C; C C C.
$endgroup$
– My_Lulu
Jan 16 at 2:54
$begingroup$
Thanks a lot for checking! I make two changes to ∧:A B A and B C B. So the definition now is: A A A; A B A; A C C; B A C; B B C; B C B; C A C; C B C; C C C.
$endgroup$
– My_Lulu
Jan 16 at 2:54
$begingroup$
@My_Lulu I'd have to check to verify that .... but I believe all you needed to change was to have A B A instead of A B C. Good work!
$endgroup$
– Bram28
Jan 16 at 3:17
$begingroup$
@My_Lulu I'd have to check to verify that .... but I believe all you needed to change was to have A B A instead of A B C. Good work!
$endgroup$
– Bram28
Jan 16 at 3:17
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3074357%2faxioms-independence-in-rosser-system%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown